mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ g₁ ≫ f₁ = g₁ ≫ f₁

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₃ ≫ f₃ = h.p₃ ≫ f₃

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p = h.p

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = φ ≫ h.p₁

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₂ = φ ≫ h.p₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₃ = φ ≫ h.p₃

Tactic:
]

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

Goal state before:
pp: case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
]

Goal state after:
case le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m_1 ↦ if x : m_1 < Opposite.unop (Opposite.op (m + 1)) then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m_1 ↦ if x : m_1 < Opposite.unop (Opposite.op (m + 1)) then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
case succ
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun m ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯ =
    functorMap f (m + 1) ≫ Pi.π (fun m_1 ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_2
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ l ≫ (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i = s.snd

Tactic:
]

Goal state after:
case refine_2
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ l ≫ (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ n
⊢ (s.π.app (Opposite.op n) ≫ (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op) ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if m < n then M m else N m) m

Tactic:
]

Goal state after:
case pos
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ n
⊢ (s.π.app (Opposite.op n) ≫ (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op) ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op) ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
]

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ ((Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op) ≫
      Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
⊢ M m = M m

Tactic:
]

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

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
⊢ M m = M m

Tactic:
]

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

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom h₁ ≫ eqToHom h₂ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m

Tactic:
]

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ functorMap f n ≫
      (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom h₁ ≫ eqToHom h₂ =
    Pi.π (fun m ↦ if m < n + 1 then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered X.hom

Tactic:
]

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered X.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫ eqToHom ⋯ ≫ eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }

Tactic:
]

Goal state after:
case e_a.le_succ_of_le
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n✝ m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < n),
    (Functor.ofOpSequence (functorMap f)).map (homOfLE hh).op ≫
        Pi.π (fun i ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun m ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : (if x : m < m + 1 then M m else N m) = if x : m < n then M m else N m
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m } ≫ eqToHom ⋯ ≫ eqToHom h₂ =
    limit.π (Discrete.functor fun m ↦ if m < n + 1 then M m else N m) { as := m }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ ((ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
]

Goal state after:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
this✝ : IsClosedUnderIsomorphisms fun f ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ ((ObjectProperty.op fun f ↦ Coequifibered f.hom).inverseImage e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ Nonempty ((md → (X ⟶ Y)) ≃ (X ⟶ yp))

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ Nonempty ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m

Tactic:
]

Goal state after:
case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n m : ℕ
h : ¬m < n
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < n then M m else N m) m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (((Pi.binaryFanOfPropIsLimit (fun m ↦ if x : m < n + 1 then M m else N m) fun m ↦ m < n + 1).conePointUniqueUpToIso
          (prodIsProd (∏ᶜ fun i ↦ if x : ↑i < n + 1 then M ↑i else N ↑i)
            (∏ᶜ fun i ↦ if x : ↑i < n + 1 then M ↑i else N ↑i))).hom ≫
      prod.map
          (Pi.map fun i ↦
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
          (Pi.map fun i ↦
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        ((Pi.binaryFanOfPropIsLimit (fun m ↦ if x : m < n then M m else N m) fun m ↦ m < n + 1).conePointUniqueUpToIso
            (prodIsProd (∏ᶜ fun i ↦ if x : ↑i < n then M ↑i else N ↑i)
              (∏ᶜ fun i ↦ if x : ↑i < n then M ↑i else N ↑i))).inv)

Tactic:
]

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝⁴ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝³ : HasCountableProducts C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasFiniteBiproducts C
inst✝ : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi
    (((Pi.binaryFanOfPropIsLimit (fun m ↦ if x : m < n + 1 then M m else N m) fun m ↦ m < n + 1).conePointUniqueUpToIso
          (prodIsProd (∏ᶜ fun i ↦ if x : ↑i < n + 1 then M ↑i else N ↑i)
            (∏ᶜ fun i ↦ if x : ↑i < n + 1 then M ↑i else N ↑i))).hom ≫
      prod.map
          (Pi.map fun i ↦
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯)
          (Pi.map fun i ↦
            if h : ↑i < n then eqToHom ⋯ else if h' : ↑i < n + 1 then eqToHom ⋯ ≫ f ↑i ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        ((Pi.binaryFanOfPropIsLimit (fun m ↦ if x : m < n then M m else N m) fun m ↦ m < n + 1).conePointUniqueUpToIso
            (prodIsProd (∏ᶜ fun i ↦ if x : ↑i < n then M ↑i else N ↑i)
              (∏ᶜ fun i ↦ if x : ↑i < n then M ↑i else N ↑i))).inv)
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (⨅ F, preservesLimit F).IsClosedUnderIsomorphisms

Tactic:
]

Goal state after:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst✝⁵ : Category.{v_1, u_5} K
inst✝⁴ : Category.{v_2, u_6} K'
inst✝³ : Category.{v_3, u_1} J
inst✝² : Category.{v_4, u_2} J'
inst✝¹ : Category.{v_5, u_3} C
inst✝ : Category.{v_6, u_4} D
⊢ (⨅ F, preservesLimit F).IsClosedUnderIsomorphisms