case h
G : Type ?u.484195
G' : Type ?u.484198
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.484207
inst✝⁴ : AddGroup A
N : Type ?u.484213
P : Type ?u.484216
inst✝³ : Group N
inst✝² : Group P
K✝ : Subgroup G
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : range f ≤ K
k : { x // x ∈ K }
⊢ k ∈ subgroupOf (range f) K ↔ k ∈ range (codRestrict f K (_ : ∀ (x : G₁), ↑f x ∈ K))
G : Type ?u.484195
G' : Type ?u.484198
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.484207
inst✝⁴ : AddGroup A
N : Type ?u.484213
P : Type ?u.484216
inst✝³ : Group N
inst✝² : Group P
K✝ : Subgroup G
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : range f ≤ K
⊢ subgroupOf (range f) K = range (codRestrict f K (_ : ∀ (x : G₁), ↑f x ∈ K))
ext k
case h
G : Type ?u.484195
G' : Type ?u.484198
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.484207
inst✝⁴ : AddGroup A
N : Type ?u.484213
P : Type ?u.484216
inst✝³ : Group N
inst✝² : Group P
K✝ : Subgroup G
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : range f ≤ K
k : { x // x ∈ K }
⊢ ∀ (a : G₁), ↑f a = ↑(Subgroup.subtype K) k ↔ ↑(codRestrict f K (_ : ∀ (x : G₁), ↑f x ∈ K)) a = k
case h
G : Type ?u.484195
G' : Type ?u.484198
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.484207
inst✝⁴ : AddGroup A
N : Type ?u.484213
P : Type ?u.484216
inst✝³ : Group N
inst✝² : Group P
K✝ : Subgroup G
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : range f ≤ K
k : { x // x ∈ K }
⊢ k ∈ subgroupOf (range f) K ↔ k ∈ range (codRestrict f K (_ : ∀ (x : G₁), ↑f x ∈ K))
refine' exists_congr _
no goals
case h
G : Type ?u.484195
G' : Type ?u.484198
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.484207
inst✝⁴ : AddGroup A
N : Type ?u.484213
P : Type ?u.484216
inst✝³ : Group N
inst✝² : Group P
K✝ : Subgroup G
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : range f ≤ K
k : { x // x ∈ K }
⊢ ∀ (a : G₁), ↑f a = ↑(Subgroup.subtype K) k ↔ ↑(codRestrict f K (_ : ∀ (x : G₁), ↑f x ∈ K)) a = k
simp [Subtype.ext_iff]