awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
⊢ Eq (α := (↑(A.prodFan B).pt : Type u))
    ((Hom.hom m : (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u)) x : (↑(A.prodFan B).pt : Type u))
    (((Hom.hom
              (ofHom
                (RingHom.prod (Hom.hom (s.π.app { as := WalkingPair.left }))
                  (Hom.hom (s.π.app { as := WalkingPair.right })))) :
            (↑s.pt : Type u) →+* (↑(A.prodFan B).pt : Type u)) :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
have hf : Eq (α := (↑(A.prodFan B).pt : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
        (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
      x :
    (↑(A.prodFan B).pt : Type u))
  (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.fst s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x,
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.snd s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x) :
    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
Tactic: change m x = (BinaryFan.fst s x, BinaryFan.snd s x)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
⊢ Eq (α := (↑(A.prodFan B).pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.fst s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.snd s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
          x) :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
have eq1 : Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          (m ≫ (A.prodFan B).fst) :
        (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
      x :
    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          (BinaryFan.fst s) :
        (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
          (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
      x :
    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
Tactic: have eq1 : (m ≫ (A.prodFan B).fst) x = (BinaryFan.fst s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.left⟩) x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
⊢ ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f = ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g
have hf : ∀ (x : (↑A : Type u)) (e : x ∈ (Hom.hom f).eqLocus (Hom.hom g)),
  Eq (α := (↑B : Type u))
    ((Hom.hom (ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f) :
          (a : (↑(of ↥((Hom.hom f).eqLocus (Hom.hom g))) : Type u)) → (↑B : Type u))
        (Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ (Hom.hom f).eqLocus (Hom.hom g)) x e) :
      (↑B : Type u))
    ((Hom.hom (ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g) :
          (a : (↑(of ↥((Hom.hom f).eqLocus (Hom.hom g))) : Type u)) → (↑B : Type u))
        (Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ (Hom.hom f).eqLocus (Hom.hom g)) x e) :
      (↑B : Type u))
Tactic: ext ⟨x, e⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
⊢ IsLimit (equalizerFork f g)
have create : (s : Fork f g) →
  { l : s.pt ⟶ (equalizerFork f g).pt //
    l ≫ (equalizerFork f g).ι = s.ι ∧ ∀ {m : s.pt ⟶ (equalizerFork f g).pt}, m ≫ (equalizerFork f g).ι = s.ι → m = l }
Tactic: fapply Fork.IsLimit.mk'
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ { l : s.pt ⟶ (equalizerFork f g).pt //
    l ≫ (equalizerFork f g).ι = s.ι ∧ ∀ {m : s.pt ⟶ (equalizerFork f g).pt}, m ≫ (equalizerFork f g).ι = s.ι → m = l }
have property : ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry) ≫ (equalizerFork f g).ι = s.ι ∧
  ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry)
Tactic: use ofHom <| s.ι.hom.codRestrict _ fun x => (ConcreteCategory.congr_hom s.condition x :)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι ∧
    ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
      m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
have property : ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry) ≫ (equalizerFork f g).ι = s.ι
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
property : ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι ∧
    ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
      m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
have property₁ : ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
  m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι
have property : ∀ (x : (↑s.pt : Type u)),
  Eq (α := (↑A : Type u))
    ((Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry) ≫ (equalizerFork f g).ι) :
          (a : (↑s.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom s.ι : (a : (↑s.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
m : s.pt ⟶ (equalizerFork f g).pt
hm : m ≫ (equalizerFork f g).ι = s.ι
⊢ m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
have property : ∀ (x : (↑s.pt : Type u)),
  Eq (α := (↑(equalizerFork f g).pt : Type u))
    ((Hom.hom m : (a : (↑s.pt : Type u)) → (↑(equalizerFork f g).pt : Type u)) x : (↑(equalizerFork f g).pt : Type u))
    ((Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) sorry)) :
          (a : (↑s.pt : Type u)) → (↑(equalizerFork f g).pt : Type u))
        x :
      (↑(equalizerFork f g).pt : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
⊢ IsLocalHom (R := (↑(equalizerFork f g).pt : Type u)) (S := (↑A : Type u)) (Hom.hom (equalizerFork f g).ι)
have map_nonunit : ∀ (a : (↑(equalizerFork f g).pt : Type u)),
  IsUnit (M := (↑A : Type u))
      ((Hom.hom (equalizerFork f g).ι : (a : (↑(equalizerFork f g).pt : Type u)) → (↑A : Type u)) a : (↑A : Type u)) →
    IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ y ∈ (Hom.hom f).eqLocus (Hom.hom g)
have apply : HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
  HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: apply (f.hom.isUnit_map ⟨⟨x, y, h₃, h₄⟩, rfl⟩ : IsUnit (f x)).mul_left_inj.mp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
| HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw : HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
  ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
  ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have conv_rhs : HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
  HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: conv_rhs => rw [h₁]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw : (Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) =
  HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw :
  (Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw₁ : Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
  ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
Tactic: rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw :
  (Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw₂ : Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
  ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
Tactic: rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw :
  (Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
rw₂ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw₃ : Eq (α := (↑B : Type u)) (1 : (↑B : Type u)) ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
Tactic: rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw :
  (Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
rw₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) (y * x) : (↑B : Type u))
rw₂ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
rw₃ : Eq (α := (↑B : Type u)) (1 : (↑B : Type u)) ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) 1 : (↑B : Type u))
⊢ HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u)) =
    HMul.hMul (α := (↑B : Type u)) (β := (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) y : (↑B : Type u))
      ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
have rw₄ : Eq.{u + 1} (α := (↑B : Type u)) 1 1
Tactic: rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ IsUnit (M := (↑(equalizerFork f g).pt : Type u))
    (Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ (Hom.hom f).eqLocus (Hom.hom g)) x h₁)
have this : y ∈ (Hom.hom f).eqLocus (Hom.hom g)
Tactic: have : y ∈ RingHom.eqLocus f.hom g.hom := by
    apply (f.hom.isUnit_map ⟨⟨x, y, h₃, h₄⟩, rfl⟩ : IsUnit (f x)).mul_left_inj.mp
    conv_rhs => rw [h₁]
    rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
x y : (↑A : Type u)
h₃ : x * y = 1
h₄ : y * x = 1
h₁ :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
    ((Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u)) x : (↑B : Type u))
this : y ∈ (Hom.hom f).eqLocus (Hom.hom g)
⊢ IsUnit (M := (↑(equalizerFork f g).pt : Type u))
    (Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ (Hom.hom f).eqLocus (Hom.hom g)) x h₁)
have map_nonunit : ∃ (b : (↑(equalizerFork f g).pt : Type u)),
  Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ (Hom.hom f).eqLocus (Hom.hom g)) x h₁ * b = 1
Tactic: rw [isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
F : WalkingParallelPair ⥤ CommRingCat
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom (limit.π F WalkingParallelPair.zero))
have this : Eq (α :=
  limit F ⟶
    (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).obj
      WalkingParallelPair.zero)
  (CategoryStruct.comp (Y :=
    limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
    (limMap (diagramIsoParallelPair F).hom)
    (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
      WalkingParallelPair.zero))
  (limit.π F WalkingParallelPair.zero ≫ (diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)
Tactic: have := limMap_π (diagramIsoParallelPair F).hom WalkingParallelPair.zero
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
F : WalkingParallelPair ⥤ CommRingCat
this :
  Eq (α :=
    limit F ⟶
      (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).obj
        WalkingParallelPair.zero)
    (CategoryStruct.comp (Y :=
      limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
      (limMap (diagramIsoParallelPair F).hom)
      (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
        WalkingParallelPair.zero))
    (limit.π F WalkingParallelPair.zero ≫ (diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom (limit.π F WalkingParallelPair.zero))
have this₁ : Eq (α := limit F ⟶ F.obj WalkingParallelPair.zero)
  (CategoryStruct.comp (Y :=
      limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
      (limMap (diagramIsoParallelPair F).hom)
      (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
        WalkingParallelPair.zero) ≫
    inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero))
  (limit.π F WalkingParallelPair.zero)
Tactic: rw [← IsIso.comp_inv_eq] at this
Cleared hypotheses: this