A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
⊢ comp 1 f = comp (QuotientGroup.mk' (range f)) f

A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' (range f)
⊢ range f = ⊤
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
⊢ range f = ⊤
specialize h 1 (QuotientGroup.mk' _) _
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ker (QuotientGroup.mk' (range f)) = ker 1
⊢ range f = ⊤
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' (range f)
⊢ range f = ⊤
replace h : (QuotientGroup.mk' _).ker = (1 : B →* B ⧸ f.range).ker := by rw [h]
no goals
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ker (QuotientGroup.mk' (range f)) = ker 1
⊢ range f = ⊤
rwa [ker_one, QuotientGroup.ker_mk'] at h
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑(comp 1 f) x = ↑(comp (QuotientGroup.mk' (range f)) f) x
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
⊢ comp 1 f = comp (QuotientGroup.mk' (range f)) f
ext1 x
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ 1 = ↑(↑f x)
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑(comp 1 f) x = ↑(comp (QuotientGroup.mk' (range f)) f) x
simp only [one_apply, coe_comp, coe_mk', Function.comp_apply]
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑f x ∈ range f
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ 1 = ↑(↑f x)
rw [show (1 : B ⧸ f.range) = (1 : B) from QuotientGroup.mk_one _, QuotientGroup.eq, inv_one,
  one_mul]
no goals
case h
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ range f), comp u f = comp v f → u = v
x : A
⊢ ↑f x ∈ range f
exact ⟨x, rfl⟩
no goals
A : Type u
B : Type v
inst✝¹ : CommGroup A
inst✝ : CommGroup B
f : A →* B
h : 1 = QuotientGroup.mk' (range f)
⊢ ker (QuotientGroup.mk' ?m.20988) = ker 1
rw [h]