mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
classical
    obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)
    let RXn := MvPolynomial (Fin n) R
    let RXm := MvPolynomial (Fin m) R
    have := fun i : Fin n => hf' (f <| X i)
    choose g hg using this
    have := fun i : Fin m => hf (f' <| X i)
    choose h hh using this
    let aeval_h : RXm →ₐ[R] RXn := aeval h
    let g' : Fin n → RXn := fun i => X i - aeval_h (g i)
    refine ⟨Finset.univ.image g' ∪ s.image aeval_h, ?_⟩
    simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]
    have hh' : ∀ x, f (aeval_h x) = f' x := by
      intro x
      rw [← f.coe_toRingHom, map_aeval]
      simp_rw [AlgHom.coe_toRingHom, hh]
      rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
        -- Porting note: added line below
        ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
        ← aeval_unique]
    let s' := Set.range g' ∪ aeval_h '' s
    have leI : Ideal.span s' ≤ RingHom.ker f.toRingHom := by
      rw [Ideal.span_le]
      rintro _ (⟨i, rfl⟩ | ⟨x, hx, rfl⟩)
      · change f (g' i) = 0
        rw [map_sub, ← hg, hh', sub_self]
      · change f (aeval_h x) = 0
        rw [hh']
        change x ∈ RingHom.ker f'.toRingHom
        rw [← hs]
        exact Ideal.subset_span hx
    apply leI.antisymm
    intro x hx
    have : x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid := by
      have : x ∈ adjoin R (Set.range X : Set RXn) := by
        rw [adjoin_range_X]
        trivial
      refine adjoin_induction ?_ ?_ ?_ ?_ this
      · rintro _ ⟨i, rfl⟩
        rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · apply Submodule.subset_span
          apply Set.mem_union_left
          exact Set.mem_range_self _
      · intro r
        apply AddSubmonoid.mem_sup_left
        exact ⟨C r, aeval_C _ _⟩
      · intro _ _ _ _ h₁ h₂
        exact add_mem h₁ h₂
      · intro p₁ p₂ _ _ h₁ h₂
        obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
        obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
        rw [mul_add, add_mul, add_assoc, ← map_mul]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)
    obtain ⟨_, ⟨x, rfl⟩, y, hy, rfl⟩ := AddSubmonoid.mem_sup.mp this
    refine add_mem ?_ hy
    simp only [RXn, RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_add,
      show f y = 0 from leI hy, add_zero, hh'] at hx
    suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h by
      apply this
      rwa [hs]
    rw [Ideal.span_le]
    intro x hx
    apply Submodule.subset_span
    apply Set.mem_union_right
    exact Set.mem_image_of_mem _ hx

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ Function.Injective ⇑f

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ Function.Injective ⇑f
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X : StructuredArrow d G
⊢ (F.map X.hom).toFunctor.obj f ⟶ (F.map X.hom).toFunctor.obj f

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X : StructuredArrow d G
⊢ (F.map X.hom).toFunctor.obj f ⟶ (F.map X.hom).toFunctor.obj f
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bi ⟶ bi

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bi ⟶ bi
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ gr.left ≫ g ≫ k = gr.right ≫ g ≫ k

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ gr.left ≫ g ≫ k = gr.right ≫ g ≫ k
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bj ⟶ bj

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ bj ⟶ bj
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : h ≫ m = h ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p

Tactic:
;

Goal state after:
case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : h ≫ m = h ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = (f ≫ h) ≫ p
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refl
C : Type u
inst✝ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f

Tactic:
;

Goal state after:
case refl
C : Type u
inst✝ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
n : ℕ
⊢ (fun x ↦ r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
;

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
n : ℕ
⊢ (fun x ↦ r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := ⋯
e₂ : Localization.Away (f r) ≃+* S' := ⋯
n : ℕ
⊢ (fun x ↦ f r ^ x) n = f ((fun x ↦ r ^ x) n)

Tactic:
;

Goal state after:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := ⋯
e₂ : Localization.Away (f r) ≃+* S' := ⋯
n : ℕ
⊢ (fun x ↦ f r ^ x) n = f ((fun x ↦ r ^ x) n)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
⊢ P (CommRingCat.Hom.hom (pushout.inl f g))

Tactic:
by
  let := f.hom.toAlgebra
  let := g.hom.toAlgebra
  rw [← show _ = pushout.inl f g from
      colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit R S T⟩ WalkingSpan.left,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]
  dsimp only [CommRingCat.pushoutCocone_inl, PushoutCocone.ι_app_left]
  apply hP R T S (S ⊗[R] T)
  exact H

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      (extendFan c₁ c₂).π.app { as := j } =
    s.π.app { as := j }

Tactic:
refine Fin.inductionOn j ?_ ?_
    · apply (BinaryFan.IsLimit.lift' t₂ _ _).2.1
    · rintro i -
      dsimp only [extendFan_π_app]
      rw [Fin.cases_succ, ← assoc, (BinaryFan.IsLimit.lift' t₂ _ _).2.2, t₁.fac]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.LimitOfShape J X✝
⊢ P.limitsOfShape J Y✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.LimitOfShape J X✝
⊢ P.limitsOfShape J Y✝
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i ↦ F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i ↦ f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i ↦ f i.succ))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
                (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π.app
          { as := i.castSucc } =
        (Iso.refl
              (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
                  (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
          (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
                  F.map
                    (Fin.cases
                      (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)))
                      (fun i ↦
                        BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)) ≫
                          (limit.cone (Discrete.functor fun i ↦ f i.succ)).π.app { as := i })
                      j)).π.app
            { as := i.castSucc } →
      (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
                (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π.app
          { as := i.succ } =
        (Iso.refl
              (extendFan (Fan.mk (F.obj (∏ᶜ fun i ↦ f i.succ)) fun j ↦ F.map (Pi.π (fun i ↦ f i.succ) j))
                  (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
          (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
                  F.map
                    (Fin.cases
                      (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)))
                      (fun i ↦
                        BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i ↦ f i.succ)).pt)) ≫
                          (limit.cone (Discrete.functor fun i ↦ f i.succ)).π.app { as := i })
                      j)).π.app
            { as := i.succ }

Tactic:
· rintro i _
      dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
      change F.map _ ≫ _ = 𝟙 _ ≫ _
      simp only [id_comp, ← F.map_comp]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯ ≫
      lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
        (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ =
    𝟙 (pullback f g)

Tactic:
by
    apply pullback.hom_ext
    · simp only [Category.assoc, lift_fst, lift_fst_assoc, lift_snd, Category.id_comp]
    · simp only [Category.assoc, lift_snd, lift_snd_assoc, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.ColimitOfShape J X✝
⊢ P.colimitsOfShape J Y✝

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝¹ : Category.{v', u'} J
J' : Type u''
inst✝ : Category.{v'', u''} J'
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.ColimitOfShape J X✝
⊢ P.colimitsOfShape J Y✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P f'

Tactic:
rw [← this] at H ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
m : c.pt ⟶ s.pt
hm : h.r ≫ m = s.π
⊢ m = h.i ≫ s.π

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
m : c.pt ⟶ s.pt
hm : h.r ≫ m = s.π
⊢ m = h.i ≫ s.π
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                  ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                    (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                  ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
              (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                    ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                    ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                      (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j =
      ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j

Tactic:
rintro ⟨_ | _⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
          tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
        (ℬ X Y).cone.π.app j =
      tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫ (ℬ X Y).cone.π.app j

Tactic:
rintro ⟨_ | _⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (j : Discrete WalkingPair),
    ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
                ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                  ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                      ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
                ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
          (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y₂ Y₃).cone.π.app j =
      (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
                ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
                ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                      ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
          (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y₂ Y₃).cone.π.app j

Tactic:
rintro ⟨_ | _⟩ <;> simp

Goal state after: