awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m :
  s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
e₁ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.fst
e₂ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.snd
x : (↑s.pt : Type u)
⊢ Eq.{u + 1} (α := (↑A : Type u) × (↑B : Type u))
    (↑((Hom.hom m :
            (a : (↑s.pt : Type u)) →
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u))
          x) :
      (↑A : Type u) × (↑B : Type u))
    (↑((Hom.hom
              (ofHom
                (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
                  ⋯)) :
            (a : (↑s.pt : Type u)) →
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u))
          x) :
      (↑A : Type u) × (↑B : Type u))
have uniq : Eq (α := (↑A : Type u) × (↑B : Type u))
  ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
            (a : (↑s.pt : Type u)) →
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u))
          x) :
      (↑A : Type u) × (↑B : Type u)) :
    (↑A : Type u) × (↑B : Type u))
  (((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x,
      (Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x) :
    (↑A : Type u) × (↑B : Type u))
Tactic: change (m x).1 = (_, _)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m :
  s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
e₁ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.fst
e₂ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.snd
x : (↑s.pt : Type u)
⊢ Eq (α := (↑A : Type u) × (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
              (a : (↑s.pt : Type u)) →
                (↑(of
                      ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                  Type u))
            x) :
        (↑A : Type u) × (↑B : Type u)) :
      (↑A : Type u) × (↑B : Type u))
    (((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x,
        (Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x) :
      (↑A : Type u) × (↑B : Type u))
have eq1 : Eq (α := (↑A : Type u))
  ((Hom.hom
          (m ≫
            ofHom
              (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
                (Subring.subtype
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) :
        (a : (↑s.pt : Type u)) → (↑A : Type u))
      x :
    (↑A : Type u))
  ((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
Tactic: have eq1 := (congr_arg (fun f : s.pt →+* A => f x) (congrArg Hom.hom e₁) :)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m :
  s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
e₁ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.fst
e₂ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.snd
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑A : Type u))
    ((Hom.hom
            (m ≫
              ofHom
                (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
                  (Subring.subtype
                    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) :
          (a : (↑s.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
⊢ Eq (α := (↑A : Type u) × (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
              (a : (↑s.pt : Type u)) →
                (↑(of
                      ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                  Type u))
            x) :
        (↑A : Type u) × (↑B : Type u)) :
      (↑A : Type u) × (↑B : Type u))
    (((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x,
        (Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x) :
      (↑A : Type u) × (↑B : Type u))
have eq2 : Eq (α := (↑B : Type u))
  ((Hom.hom
          (m ≫
            ofHom
              (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
                (Subring.subtype
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) :
        (a : (↑s.pt : Type u)) → (↑B : Type u))
      x :
    (↑B : Type u))
  ((Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: have eq2 := (congr_arg (fun f : s.pt →+* B => f x) (congrArg Hom.hom e₂) :)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S
have simp_rw : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
Tactic: simp_rw [Algebra.isEpi_iff_forall_one_tmul_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
have mp : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) → ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
mp : Epi (X := of R) (Y := of S) (ofHom (algebraMap 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)) ↔ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
have mpr : (∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)) → Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
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 (α := of R ⟶ of (S ⊗[R] S))
    (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S)) (ofHom Algebra.TensorProduct.includeLeftRingHom))
    (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
      (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)))
have hf : ∀ (r : (↑(of R) : Type u)),
  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: ext r
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
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 (α := (↑(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))
have 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)
Tactic: change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (hypothesis)
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))
⊢ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
have this : 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])
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
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))
have 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
Tactic: refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
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' := ⋯ }
⊢ f = g
have 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))
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
inst : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
⊢ 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))
have algebraizeInst : Module.Finite.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
Tactic: algebraize [f.hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (hypothesis)
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)
⊢ 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))
have this : 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)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Epi (goal)
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)
⊢ 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))
have 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))
Tactic: rwa [Algebra.isEpi_iff_surjective_algebraMap_of_finite] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.EqualizerPushout (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
⊢ IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (Fork.ofι f ⋯)
have algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [f.hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.EqualizerPushout (goal)
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)
⊢ 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)))
have 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)))
Tactic: rw [(PushoutCocone.condition _)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
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
have 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
Tactic: refine Quot.inductionOn x ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨j, x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x : (↑(R.{v, u} F) : Type (max u v))
⊢ x * 0 = 0
have 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),
  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
Tactic: refine Quot.inductionOn x ?_