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

Goal state before:
pp: case star.star
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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ (f : WithTerminal.star ⟶ WithTerminal.star),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
try rintro ⟨⟩

Goal state after:
case star.star
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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ (WithTerminal.liftFromOver.obj c).map PUnit.unit ≫
      (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
    (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt

Tactic:
simpa using PushoutCocone.condition s

Goal state after:
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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ (Cone.postcompose
          (NatIso.ofComponents
              (fun i ↦
                WithTerminal.casesOn i (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                  (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
              ⋯).hom).obj
      (WithTerminal.coneEquiv.functor.obj { pt := G, π := α }) ≅
    (Over.forget F).mapCone
      { pt := G,
        π :=
          {
            app := fun i ↦
              WithTerminal.casesOn i α.app
                (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
            naturality := ⋯ } }

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
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
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
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ (Cone.postcompose
          (NatIso.ofComponents
              (fun i ↦
                WithTerminal.casesOn i (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
                  (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star)))
              ⋯).hom).obj
      (WithTerminal.coneEquiv.functor.obj { pt := G, π := α }) ≅
    (Over.forget F).mapCone
      { pt := G,
        π :=
          {
            app := fun i ↦
              WithTerminal.casesOn i α.app
                (Over.mkIdTerminal.from (((const (WithTerminal J)).obj G).obj WithTerminal.star)),
            naturality := ⋯ } }
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
n m : ℕ
h : m < n
⊢ m < n

Tactic:
by lia

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
n m : ℕ
h : ¬m < n
⊢ ¬m < n

Tactic:
by lia

Goal state after:
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
n m : ℕ
h : m < n
h✝ : ¬m < n + 1
⊢ N m = M m

Tactic:
try lia

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

Goal state before:

Tactic:
try lia

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
n : ℕ
⊢ n ≤ n + 1

Tactic:
by lia

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
n : ℕ
⊢ ¬n < n

Tactic:
by lia

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
n : ℕ
⊢ n < n + 1

Tactic:
by lia

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
n m k : ℕ
h : n ≤ m
hh : ¬k < m
⊢ ¬k < n

Tactic:
by lia

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
n m✝ k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    (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 ⋯
hh : ¬k < m + 1
⊢ ¬k < m

Tactic:
by lia

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
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 ⋯
⊢ n ≤ m + 1

Tactic:
by lia

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
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 ⋯
⊢ n ≤ m

Tactic:
by lia

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
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 ⋯
⊢ m ≤ m + 1

Tactic:
by lia

Goal state after:
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
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 ⋯
h✝ : k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

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
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 ⋯
h✝ : ¬k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

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
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 ⋯
h✝ : k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯
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
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 ⋯
h✝ : ¬k < m
⊢ ¬k < m

Tactic:
by lia

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
n m : ℕ
h : ¬m < n
⊢ n ≤ m + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m < n
⊢ m < m + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1 + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m + 1 < n
⊢ m + 1 ≤ m + 1 + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ n ≤ m + 1

Tactic:
by lia

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
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ¬m + 1 < m + 1

Tactic:
by lia

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

Goal state before:
pp: case isTrue
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 < n
⊢ Pi.π M m ≫ eqToHom ⋯ = Pi.π M m ≫ (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫ eqToHom ⋯

pp: case isFalse
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 < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
·

Goal state after:
case isTrue
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 < n
⊢ Pi.π M m ≫ eqToHom ⋯ = Pi.π M m ≫ (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫ eqToHom ⋯
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
n m : ℕ
h✝ : m < n
⊢ m < n + 1

Tactic:
by lia

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

Goal state before:
pp: case isFalse
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 < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯

Tactic:
·

Goal state after:
case isFalse
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 < n
⊢ Pi.π M m ≫ f m ≫ eqToHom ⋯ =
    Pi.π M m ≫
      (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫
        if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯
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
m n : ℕ
h : ¬n < m
⊢ (cone f).π.app (Opposite.op m) ≫ Pi.π (fun m_1 ↦ if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n =
    Pi.π M n ≫ f n ≫ eqToHom ⋯

Tactic:
by
  simp [cone_π_app, dif_neg h]

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))
m : ℕ
⊢ m < m + 1

Tactic:
by lia

Goal state after:
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
⊢ ((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 ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m

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 ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op 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
⊢ ((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 ⋯) ≫
        (cone f).π.app (Opposite.op n)) ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m =
    s.π.app (Opposite.op n) ≫ Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op 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
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 + 1

Tactic:
by lia

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 ⋯
⊢ m < n

Tactic:
by lia

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 < n

Tactic:
by lia

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
h₂ : (if x : m < n then M m else N m) = if x : m < n + 1 then M m else N m
⊢ m < n

Tactic:
by lia

Goal state after:
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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ Cardinal.{u}

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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ 2 ^ α ≤ ?m.56

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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ ?m.56 ≤ α

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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ Cardinal.{u}
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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ 2 ^ α ≤ #(X ⟶ yp)

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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(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 := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ 2 ^ α ≤ #(X ⟶ yp)