mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ f = p.map φ

Tactic:
simpa using h.symm

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom
        ((Types.binaryProductIso ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.left })
              ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.right })).inv ≫
          ((Cone.postcomposeEquivalence (diagramIsoPair (pair X Y ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                ((isLimitOfPreserves (F ⋙ FintypeCat.incl) (prodIsProd X Y)).liftConeMorphism
                  ((Cone.postcomposeEquivalence (diagramIsoPair (pair X Y ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (pair ((F ⋙ FintypeCat.incl).obj X) ((F ⋙ FintypeCat.incl).obj Y)))))).hom ≫
            (F ⋙ FintypeCat.incl).map prod.snd))
      (x, y) =
    y

Tactic:
erw [PreservesLimitPair.iso_inv_snd, Types.binaryProductIso_inv_comp_snd]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (↾_root_.Prod.snd)) (x, y) = y
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
induction n using Nat.strongRecOn with | _ n hi
   =>  _ 

Goal state after:
case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), IsConnected (f i)

Tactic:
by
  obtain ⟨ι, f, g, hl, hc, hf⟩ := has_decomp_connected_components X
  exact ⟨ι, hf, f, colimit.isoColimitCocone ⟨Cofan.mk X g, hl⟩, hc⟩

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ S ∈ 𝓝 1 ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

Tactic:
rw [mem_nhds_iff]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) ↔ ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).obj
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
rw [mem_nhds_iff]

Goal state after:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : (X : C) → MulAction G (F.obj X).obj
inst✝⁵ : IsNaturalSMul F G
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ∃ t ⊆ ⇑(toAut F G) ⁻¹' A, IsOpen t ∧ 1 ∈ t
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
⊢ (of C ⋙ lift φ).toPrefunctor = φ.toPrefunctor

Tactic:
change Quiver.FreeGroupoid.of C ⋙q
      (Quotient.functor (FreeGroupoid.homRel C)).toPrefunctor ⋙q
        (lift φ).toPrefunctor = φ.toPrefunctor
    simp [lift, Quotient.lift_spec, Quiver.FreeGroupoid.lift_spec]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)

Tactic:
choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))

Goal state after:
C : Type u₁
inst✝⁵ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁴ : GaloisCategory C
inst✝³ : FiberFunctor F
X : Action FintypeCat (Aut F)
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul (Aut F) X.V.obj
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun i ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i)))) ≅ X
g : ι → C
gu :
  ∀ (i : ι),
    Nonempty ((functorToAction F).obj (g i) ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑(f i))))
⊢ ∃ A, Nonempty ((functorToAction F).obj A ≅ X)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
⊢ c ∈ S.objs → 𝟙 c ∈ S.arrows c c

Tactic:
rintro ⟨γ, hγ⟩

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
x✝¹ : Fan fun x ↦ U
x✝ : α
⊢ { f := fun i a ↦ (x✝¹.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (x✝¹.proj a).φ i } ≫ (U.powerFan α).proj x✝ =
    x✝¹.proj x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
⊢ powerMap (f ≫ g) α = powerMap f α ≫ powerMap g α

Tactic:
ext
  · cat_disch
  · dsimp
    ext
    simp only [Category.comp_id, Category.assoc, Pi.map_π, Function.comp_apply,
      Pi.map_π_assoc]
    apply Pi.map_π

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
U : FormalCoproduct C
α β : Type
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
f : α → β
a : α
⊢ U.mapPower f ≫ U.powerπ a = U.powerπ (f a)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
𝒜 : Type w
f : 𝒜 → FormalCoproduct C
t X : FormalCoproduct C
p : (i : 𝒜) → f i ⟶ t
⊢ (fun m i ↦ (cofan 𝒜 f).inj i ≫ m) ((fun s ↦ { f := fun p ↦ (s p.fst).f p.snd, φ := fun p ↦ (s p.fst).φ p.snd }) p) = p

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
⊢ (fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩)
      ((fun s ↦
          { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
            φ := fun i ↦ (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
        s) =
    s

Tactic:
ext <;> simp

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:
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:
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:
lia

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

Goal state before:

Tactic:
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:
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:
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:
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:
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:
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:
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:
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:
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 ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
h✝ : ¬k < m
⊢ ¬k < m

Tactic:
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
⊢ (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 ⋯

Tactic:
by
  induction h using Nat.leRec with
  | refl => simp
  | @le_succ_of_le m h ih =>
    specialize ih (by lia)
    have : homOfLE (by lia : n ≤ m + 1) =
        homOfLE (by lia : n ≤ m) ≫ homOfLE (by lia : m ≤ m + 1) := by simp
    rw [this, op_comp, Functor.map_comp]
    slice_lhs 2 4 => rw [ih]
    simp only [homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, dite_eq_ite]
    split_ifs
    · omega
    simp [dif_neg (by lia : ¬(k < m)), dif_neg hh]

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

Tactic:
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:
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:
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:
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:
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:
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 + 1

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

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

Tactic:
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 < m + 1

Tactic:
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:
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:
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:
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))
m : s.pt ⟶ (cone f).pt
h : ∀ (j : ℕᵒᵖ), m ≫ (cone f).π.app j = s.π.app j
n : ℕ
⊢ n < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, u'} J
⊢ ObjectProperty.preservesLimitsOfShape J = (⨆ F, MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal

Tactic:
by
  simp only [ObjectProperty.preservesLimitsOfShape_eq_iSup,
    MorphismProperty.isLocal_iSup, preservesLimit_eq_isLocal]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ W₁.IsMultiplicative

Tactic:
rw [hW₁]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
⊢ { fst := whiskerRight (𝟙 X✝) (π₁ F G), snd := whiskerRight (𝟙 X✝) (π₂ F G), w := ⋯ } =
    𝟙
      { fst := X✝ ⋙ π₁ F G, snd := X✝ ⋙ π₂ F G,
        iso :=
          X✝.associator (π₁ F G) F ≪≫
            X✝.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X✝.associator (π₂ F G) G).symm }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { fst := whiskerRight (f✝ ≫ g✝) (π₁ F G), snd := whiskerRight (f✝ ≫ g✝) (π₂ F G), w := ⋯ } =
    { fst := whiskerRight f✝ (π₁ F G), snd := whiskerRight f✝ (π₂ F G), w := ⋯ } ≫
      { fst := whiskerRight g✝ (π₁ F G), snd := whiskerRight g✝ (π₂ F G), w := ⋯ }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : CatCommSqOver F G X
⊢ { app := fun x ↦ { fst := (𝟙 X✝).fst.app x, snd := (𝟙 X✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    𝟙
      { obj := fun x ↦ { fst := X✝.fst.obj x, snd := X✝.snd.obj x, iso := X✝.iso.app x },
        map := fun {x y} f ↦ { fst := X✝.fst.map f, snd := X✝.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ Z✝ : CatCommSqOver F G X
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ { fst := (f✝ ≫ g✝).fst.app x, snd := (f✝ ≫ g✝).snd.app x, w := ⋯ }, naturality := ⋯ } =
    { app := fun x ↦ { fst := f✝.fst.app x, snd := f✝.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
      { app := fun x ↦ { fst := g✝.fst.app x, snd := g✝.snd.app x, w := ⋯ }, naturality := ⋯ }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ Y✝ : X ⥤ F ⊡ G
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (X ⥤ F ⊡ G)).map f✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y✝).obj x).snd) ⋯)
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X✝).obj x).snd) ⋯)
          ⋯).hom ≫
      (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).map f✝

Tactic:
ext <;> simp

Goal state after: