awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
r : (↑(of R) : Type u)
hf :
  Eq (α := S ⊗[R] S) ((algebraMap R S : (a : R) → S) r ⊗ₜ[R] 1 : S ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) r : S ⊗[R] S)
⊢ Eq (α := (↑(of (S ⊗[R] S)) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
              (ofHom Algebra.TensorProduct.includeLeftRingHom)) :
          (a : (↑(of R) : Type u)) → (↑(of (S ⊗[R] S)) : Type u))
        r :
      (↑(of (S ⊗[R] S)) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
              (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))) :
          (a : (↑(of R) : Type u)) → (↑(of (S ⊗[R] S)) : Type u))
        r :
      (↑(of (S ⊗[R] S)) : Type u))

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

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
r : (↑(of R) : Type u)
⊢ Eq (α := S ⊗[R] S) ((algebraMap R S : (a : R) → S) r ⊗ₜ[R] 1 : S ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) r : S ⊗[R] S)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
⊢ Eq.{u + 1} (α := of S ⟶ of (S ⊗[R] S)) (ofHom Algebra.TensorProduct.includeLeftRingHom)
    (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))

Tactic:
have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom)
      (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
      (by ext r; change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
          simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
this :
  Eq.{u + 1} (α := of S ⟶ of (S ⊗[R] S)) (ofHom Algebra.TensorProduct.includeLeftRingHom)
    (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
⊢ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)

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

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
this :
  Eq.{u + 1} (α := of S ⟶ of (S ⊗[R] S)) (ofHom Algebra.TensorProduct.includeLeftRingHom)
    (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))
⊢ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)

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

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ (∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)) → Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))

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

Premises used: CategoryTheory.Epi.mk
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
mpr :
  ∀ (H : ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)) {T : CommRingCat.{u}} (f g : of S ⟶ T)
    (e : Eq (α := of R ⟶ T) (ofHom (algebraMap R S) ≫ f) (ofHom (algebraMap R S) ≫ g)), f = g
⊢ (∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)) → Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))

Tactic:
refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
T : CommRingCat
f g : of S ⟶ T
e : Eq (α := of R ⟶ T) (ofHom (algebraMap R S) ≫ f) (ofHom (algebraMap R S) ≫ g)
this : Algebra R (↑T : Type u) := RingHom.toAlgebra (Hom.hom (ofHom (algebraMap R S) ≫ g))
f' : S →ₐ[R] (↑T : Type u) := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] (↑T : Type u) := { toRingHom := Hom.hom g, commutes' := ⋯ }
mpr :
  ∀ (s : (↑(of S) : Type u)),
    Eq (α := (↑T : Type u)) ((Hom.hom f : (a : (↑(of S) : Type u)) → (↑T : Type u)) s : (↑T : Type u))
      ((Hom.hom g : (a : (↑(of S) : Type u)) → (↑T : Type u)) s : (↑T : Type u))
⊢ f = g

Tactic:
ext s
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
T : CommRingCat
f g : of S ⟶ T
e : Eq (α := of R ⟶ T) (ofHom (algebraMap R S) ≫ f) (ofHom (algebraMap R S) ≫ g)
this : Algebra R (↑T : Type u) := RingHom.toAlgebra (Hom.hom (ofHom (algebraMap R S) ≫ g))
f' : S →ₐ[R] (↑T : Type u) := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] (↑T : Type u) := { toRingHom := Hom.hom g, commutes' := ⋯ }
s : (↑(of S) : Type u)
⊢ Eq (α := (↑T : Type u)) ((Hom.hom f : (a : (↑(of S) : Type u)) → (↑T : Type u)) s : (↑T : Type u))
    ((Hom.hom g : (a : (↑(of S) : Type u)) → (↑T : Type u)) s : (↑T : Type u))

Tactic:
simpa using congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : CommRingCat
f : R ⟶ S
inst : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
⊢ Module.Finite.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)

Tactic:
algebraize [f.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : CommRingCat
f : R ⟶ S
inst : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst : Module.Finite.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
⊢ Algebra.IsEpi.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)

Tactic:
have : Algebra.IsEpi R S := CommRingCat.epi_iff_epi.mp <| inferInstanceAs (Epi f)
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : CommRingCat
f : R ⟶ S
inst : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst : Module.Finite.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
this : Algebra.IsEpi.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Function.Surjective.{u_1 + 1, u_1 + 1} (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
        (⇑(algebraMap (↑R : Type u_1) (↑S : Type u_1)) : (a : (↑R : Type u_1)) → (↑S : Type u_1))),
    Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) f) :
        (a : (↑R : Type u_1)) → (↑S : Type u_1))
⊢ Function.Surjective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))

Tactic:
rwa [Algebra.isEpi_iff_surjective_algebraMap_of_finite] at this

Premises used: Algebra.isEpi_iff_surjective_algebraMap_of_finite
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
⊢ Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [f.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
rw rw₁ :
  Eq.{u + 1} (α :=
    of (↑R : Type u) ⟶
      Cocone.pt (F :=
        span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
          (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
        (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (ofHom (algebraMap (↑R : Type u) (↑S : Type u)) ≫
      PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (ofHom (algebraMap (↑R : Type u) (↑S : Type u)) ≫
      PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
⊢ Eq.{u + 1} (α :=
    of (↑R : Type u) ⟶
      Cocone.pt (F :=
        span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
          (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
        (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (ofHom (algebraMap (↑R : Type u) (↑S : Type u)) ≫
      PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
    (ofHom (algebraMap (↑R : Type u) (↑S : Type u)) ≫
      PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))

Tactic:
rw [(PushoutCocone.condition _)]

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
fork : Fork (X := of (↑S : Type u)) (Y :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  Fork.ofι (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ⋯
isPushout : IsPushout.{u, u + 1} (Z := of (↑R : Type u)) (X := of (↑S : Type u)) (Y := of (↑S : Type u)) (P :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  ⋯
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Iso.hom (Iso.refl (of (↑S : Type u))) ≫ PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) =
    PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
              (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))
⊢ Iso.hom (Iso.refl (of (↑S : Type u))) ≫ PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) =
    PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
              (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
fork : Fork (X := of (↑S : Type u)) (Y :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  Fork.ofι (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ⋯
isPushout : IsPushout.{u, u + 1} (Z := of (↑R : Type u)) (X := of (↑S : Type u)) (Y := of (↑S : Type u)) (P :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  ⋯
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Iso.hom (Iso.refl (of (↑S : Type u))) ≫ PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) =
    PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
              (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))
⊢ Iso.hom (Iso.refl (of (↑S : Type u))) ≫ PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) =
    PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
              (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
fork : Fork (X := of (↑S : Type u)) (Y :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  Fork.ofι (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ⋯
isPushout : IsPushout.{u, u + 1} (Z := of (↑R : Type u)) (X := of (↑S : Type u)) (Y := of (↑S : Type u)) (P :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  ⋯
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  (RingEquiv.toCommRingCatIso
          (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone (↑R : Type u) (↑S : Type u)) ⋯)).hom ≫
      Fork.ι
        (equalizerFork (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
          (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))) =
    fork.ι ≫ Iso.hom (Iso.refl (of (↑S : Type u)))
⊢ (RingEquiv.toCommRingCatIso
          (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone (↑R : Type u) (↑S : Type u)) ⋯)).hom ≫
      Fork.ι
        (equalizerFork (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
          (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))) =
    fork.ι ≫ Iso.hom (Iso.refl (of (↑S : Type u)))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
⊢ IsRegularMono f

Tactic:
isRegularMono_of_regularMono (regularMonoOfFaithfullyFlat f hf)

Premises used: CategoryTheory.isRegularMono_of_regularMono, CommRingCat.regularMonoOfFaithfullyFlat
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCatᵒᵖ
f : S ⟶ R
hf : (Hom.hom f.unop).FaithfullyFlat
⊢ IsRegularEpi f

Tactic:
(isRegularEpi_op_iff_isRegularMono _).mpr (isRegularMono_of_faithfullyFlat _ hf)

Premises used: Iff.mpr, CommRingCat.isRegularMono_of_faithfullyFlat, Quiver.Hom.op, CategoryTheory.isRegularEpi_op_iff_isRegularMono
-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCatᵒᵖ
f : S ⟶ R
hf : (Hom.hom f.unop).FaithfullyFlat
⊢ EffectiveEpi f

Tactic:
(isRegularEpi_iff_effectiveEpi _).mp (regularEpiOfFaithfullyFlat _ hf)

Premises used: CategoryTheory.isRegularEpi_iff_effectiveEpi, Iff.mp, CommRingCat.Opposite.regularEpiOfFaithfullyFlat
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x : (↑(R.{v, u} F) : Type (max u v))
⊢ 0 * x = 0

Tactic:
Quot.inductionOn x ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x : (↑(R.{v, u} F) : Type (max u v))
refine :
  ∀
    (a :
      (j : J) ×
        ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).obj
          j),
    0 *
        Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          a =
      0
⊢ 0 * x = 0

Tactic:
refine Quot.inductionOn x ?_
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x :
  (j : J) ×
    ((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
              MonCat.carrier)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j
obtain :
  ∀ (j : J)
    (x :
      ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).obj
        j),
    0 *
        Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x) =
      0
⊢ 0 *
      Quot.mk
        ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        x =
    0

Tactic:
obtain ⟨j, x⟩ := x
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
j : J
x :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j
⊢ MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j 0) =
    AddMonCat.FilteredColimits.M.mk
      ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
        forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommMonCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
                (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j 0)

Tactic:
rfl