-- Mathlib/Algebra/Category/Ring/Epi.lean
lemma CommRingCat.epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
    Epi (CommRingCat.ofHom (algebraMap R S)) ↔
      ∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s

Proof state:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
⊢ f = g

Tactic:
ext s

Result:
case mpr.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
s : ↑(of S)
⊢ (Hom.hom f) s = (Hom.hom g) s

Proof state:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
⊢ f = g

Tactic:
let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩

Result:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
⊢ f = g

Proof state:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
⊢ f = g

Tactic:
letI : Algebra R T := (ofHom (algebraMap R S) ≫ g).hom.toAlgebra

Result:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
⊢ f = g

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
⊢ ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext r

Result:
case hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
constructor

Result:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s) → Epi (ofHom (algebraMap R S))

Proof state:
case mpr.hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
s : ↑(of S)
⊢ (Hom.hom f) s = (Hom.hom g) s

Tactic:
simpa using congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))

Result:
no goals

Proof state:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
intro H

Result:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
⊢ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Proof state:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
this : ofHom Algebra.TensorProduct.includeLeftRingHom = ofHom Algebra.TensorProduct.includeRight.toRingHom
⊢ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
exact RingHom.congr_fun (congrArg Hom.hom this)

Result:
no goals

Proof state:
case hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (algebraMap R S) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) r

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul]

Result:
no goals

Proof state:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
⊢ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom (R := R))
  (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
  (by ext r; show algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
      simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])

Result:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
this : ofHom Algebra.TensorProduct.includeLeftRingHom = ofHom Algebra.TensorProduct.includeRight.toRingHom
⊢ ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Proof state:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
⊢ f = g

Tactic:
let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩

Result:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
⊢ f = g

Proof state:
case hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
show algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r

Result:
case hf.a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (algebraMap R S) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) r

Proof state:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s) → Epi (ofHom (algebraMap R S))

Tactic:
refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩

Result:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
⊢ f = g