awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
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))
⊢ ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ f = ofHom ((Hom.hom f).eqLocus (Hom.hom g)).subtype ≫ g

Tactic:
ext ⟨x, e⟩
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
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:
simpa using e
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
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 }
⊢ IsLimit (equalizerFork f g)

Tactic:
fapply Fork.IsLimit.mk'

Premises used: CategoryTheory.Limits.Fork.IsLimit.mk'
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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.ι ∧
    ∀ {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)) ⋯)
⊢ { 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:
use ofHom <| s.ι.hom.codRestrict _ fun x => (ConcreteCategory.congr_hom s.condition x :)

Premises used: CommRingCat.Hom.hom, CommRingCat.ofHom, CategoryTheory.Limits.Fork.ι, RingHom.codRestrict
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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.ι
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)) ⋯)
⊢ 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)) ⋯)

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
property :
  ∀ (x : (↑s.pt : Type u)),
    Eq (α := (↑A : Type u))
      ((Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (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))
⊢ ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (equalizerFork f g).ι = s.ι

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
x : (↑s.pt : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯) ≫ (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:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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.ι
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)) ⋯)) :
            (a : (↑s.pt : Type u)) → (↑(equalizerFork f g).pt : Type u))
          x :
        (↑(equalizerFork f g).pt : Type u))
⊢ m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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.ι
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)) ⋯)) :
          (a : (↑s.pt : Type u)) → (↑(equalizerFork f g).pt : Type u))
        x :
      (↑(equalizerFork f g).pt : Type u))

Tactic:
Subtype.ext <| RingHom.congr_fun (congrArg Hom.hom hm) x

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun, Subtype.ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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.ι
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)) ⋯)) :
          (a : (↑s.pt : Type u)) → (↑(equalizerFork f g).pt : Type u))
        x :
      (↑(equalizerFork f g).pt : Type u))

Tactic:
exact Subtype.ext <| RingHom.congr_fun (congrArg Hom.hom hm) x

Premises used: CommRingCat.Hom.hom, congrArg, RingHom.congr_fun, Subtype.ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
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
⊢ IsLocalHom (R := (↑(equalizerFork f g).pt : Type u)) (S := (↑A : Type u)) (Hom.hom (equalizerFork f g).ι)

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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))
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))
⊢ y ∈ (Hom.hom f).eqLocus (Hom.hom g)

Tactic:
apply (f.hom.isUnit_map ⟨⟨x, y, h₃, h₄⟩, rfl⟩ : IsUnit (f x)).mul_left_inj.mp

Premises used: CommRingCat.Hom.hom, Units.mk, Exists.intro, Iff.mp, RingHom.isUnit_map, IsUnit.mul_left_inj, rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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 :
  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 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:
rw [h₁]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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))
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))
⊢ 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:
conv_rhs => rw [h₁]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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))
rw₄ rw₅ : Eq.{u + 1} (α := (↑B : Type u)) 1 1
⊢ 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:
rw [← f.hom.map_mul, ← g.hom.map_mul, h₄, f.hom.map_one, g.hom.map_one]

Premises used: CommRingCat.Hom.hom, RingHom.map_one, RingHom.map_mul
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)

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]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)
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
⊢ 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₁)

Tactic:
rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)
⊢ ∃ (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:
⟨⟨y, this⟩, Subtype.ext h₃⟩

Premises used: Subtype.mk, Exists.intro, Subtype.ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)
⊢ ∃ (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:
exact ⟨⟨y, this⟩, Subtype.ext h₃⟩
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
F : WalkingParallelPair ⥤ CommRingCat
⊢ 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
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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)
⊢ 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

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
F : WalkingParallelPair ⥤ CommRingCat
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)
rw :
  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
      (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)))
⊢ 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))

Tactic:
rw [← this]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
F : WalkingParallelPair ⥤ CommRingCat
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)
⊢ IsLocalHom (R := (↑(Functor.obj lim F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(Functor.obj lim F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom
      ((CategoryTheory.Functor.map lim (diagramIsoParallelPair F).hom ≫
          CategoryStruct.comp (Y :=
            Cone.pt (F := parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
              (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
            (Iso.hom
                (limit.isoLimitCone
                  { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                    isLimit :=
                      equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) }) :
              limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) ⟶
                Cone.pt (F := parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
                  (LimitCone.cone
                    { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                      isLimit :=
                        equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                          (F.map WalkingParallelPairHom.right) }))
            (Fork.ι (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
⊢ CategoryStruct.comp (Y := limit (walkingParallelPairOpEquiv.functor ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOpEquiv.functor (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOpEquiv.functor ⋙ F) }))
      (limit.π (walkingParallelPairOpEquiv.functor ⋙ F) zero) =
    { cone := Cone.whisker walkingParallelPairOpEquiv.functor (limit.cone F),
              isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv }.cone.π.app
      zero

Tactic:
have := limit.isoLimitCone_inv_π
    ⟨_, IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv⟩
        WalkingParallelPair.zero
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this :
  CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero) =
    limit.π F (op one)
rw :
  IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
        (Iso.inv
          (limit.isoLimitCone
            { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
              isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
              LimitCone (walkingParallelPairOp ⋙ F) }))
        (limit.π (walkingParallelPairOp ⋙ F) zero)))
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj (op one)) : Type u)) (Hom.hom (limit.π F (op one)))

Tactic:
rw [← this]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this :
  CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero) =
    limit.π F (op one)
⊢ IsLocalHom (R := (↑(limit (walkingParallelPairOp ⋙ F)) : Type u)) (S :=
    (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u)) (F :=
    (↑(limit (walkingParallelPairOp ⋙ F)) : Type u) →+* (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u))
    (Hom.hom (limit.π (walkingParallelPairOp ⋙ F) zero))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this :
  CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero) =
    limit.π F (op one)
⊢ IsLocalHom (R := (↑(limit (walkingParallelPairOp ⋙ F)) : Type u)) (S :=
    (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u)) (F :=
    (↑(limit (walkingParallelPairOp ⋙ F)) : Type u) →+* (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u))
    (Hom.hom (limit.π (walkingParallelPairOp ⋙ F) zero))

Tactic:
have : IsLocalHom (limit.π (walkingParallelPairOp ⋙ F) zero).hom := by infer_instance