mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : k < i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.succ k ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : ι → ↑(ofHoms f).toSet := fun i ↦ ⟨Arrow.mk (f i), ⋯⟩
⊢ Function.Surjective φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm ((equivShrink ↑W.toSet) ⟨Arrow.mk f, hf⟩))).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W ↔ ∃ ι A B f, W = ofHoms f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hki).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
x✝ : (i : α) × ↑(W i).toSet
i : α
f : ↑(W i).toSet
⊢ ↑f ∈ ⋃ i, (W i).toSet

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
⊢ Small.{w, max u v} ↑(iSup W).toSet

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e e' : d.Extension val₀ j
h : e.val = e'.val
⊢ e = e'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type t
inst✝¹ : Small.{w, t} α
W : α → MorphismProperty C
inst✝ : ∀ (i : α), IsSmall.{w, v, u} (W i)
⊢ IsSmall.{w, v, u} (⨆ i, W i)

Tactic:
choose α A B f hf using fun i ↦ (isSmall_iff_eq_ofHoms.{w} (W i)).1 inferInstance

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α✝ : Type t
inst✝¹ : Small.{w, t} α✝
W : α✝ → MorphismProperty C
inst✝ : ∀ (i : α✝), IsSmall.{w, v, u} (W i)
α : α✝ → Type w
A B : (i : α✝) → α i → C
f : (i : α✝) → (i_1 : α i) → A i i_1 ⟶ B i i_1
hf : ∀ (i : α✝), W i = ofHoms (f i)
⊢ IsSmall.{w, v, u} (⨆ i, W i)
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type t
inst✝¹ : Small.{w, t} α
W : α → MorphismProperty C
inst✝ : ∀ (i : α), IsSmall.{w, v, u} (W i)
⊢ IsSmall.{w, v, u} (⨆ i, W i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
⊢ i ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
⊢ i ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
⊢ Subsingleton (d.Extension val₀ j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
e : d.Extension val₀ j
i : J
e' : d.Extension val₀ i
h : i ≤ j
⊢ (ConcreteCategory.hom (F.map (homOfLE h).op)) e.val = e'.val

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀ = val₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : i < ⊥
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀ = d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ i = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ f ≫ p = c.ι.app ⊥ ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
inst✝ : SuccOrder J
⊢ sq'.f' ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app (Order.succ j) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
j' : J
α : j' ⟶ j
⊢ F.map (homOfLE ⋯) ≫ F.map α ≫ sq'.f' = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
hi : Order.IsSuccLimit ⊥
hij : ⊥ ≤ ⊥
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) val₀ =
    d.lift ⊥ hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀,
        ⋯⟩

Tactic:
simpa using hi.not_isMin

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ ⊥
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) val₀ =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀,
        ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g✝).sections
i i' : ↑(Set.Iio j)
g : i ⟶ i'
⊢ (⋯.functor ⋙ F).map g ≫ (↑s (Opposite.op i')).f' =
    (↑s (Opposite.op i)).f' ≫ ((Functor.const ↑(Set.Iio j)).obj X).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
⊢ ⊥ ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) = val₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
x✝ : ↑(Set.Iio j)
i : J
hij : i ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone F).ι.app ⟨i, hij⟩ ≫ liftHom hj s ≫ p =
    ((Set.principalSegIio j).cocone F).ι.app ⟨i, hij⟩ ≫ c.ι.app (Opposite.unop (Opposite.op j)) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
i : J
hij : i < j
⊢ SqStruct.map (lift hj s) (homOfLE ⋯) = ↑s (Opposite.op ⟨i, hij⟩)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : i < Order.succ j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, c.incl.app b ≫ φ₁ = c.incl.app b ≫ φ₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₁ =
    ((Set.principalSegIio j).cocone c.F).ι.app ⟨k, hk⟩ ≫ c.incl.app j ≫ φ₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this✝ : ∀ (sq : CommSq sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ F.map (homOfLE ⋯) ≫ ⋯.lift = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c : RelativeCellComplex basicCell f
Z : C
φ₁ φ₂ : Y ⟶ Z
h₀ : f ≫ φ₁ = f ≫ φ₂
h : ∀ (γ : c.Cells), γ.ι ≫ φ₁ = γ.ι ≫ φ₂
⊢ φ₁ = φ₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
⊢ (ConcreteCategory.hom ((sqFunctor c p f g).map (homOfLE ⋯).op))
      (have this := ⋯;
      have this_1 := ⋯;
      { f' := ⋯.lift, w₁ := ⋯, w₂ := ⋯ }) =
    sq'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c✝ : RelativeCellComplex basicCell f
c : RelativeCellComplex basicCell f
I : MorphismProperty C
hc : ∀ (s : c.Cells), I (basicCell s.j s.i)
j : J
hj : ¬IsMax j
⊢ (coproducts.{w, v, u} I).pushouts (c.F.map (homOfLE ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
sq : CommSq f (c.ι.app ⊥) p g✝
s : ↑(sqFunctor c p f g✝).sections
hs : (↑s (Opposite.op ⊥)).f' = f
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ (↑s (Opposite.op j')).f' = (↑s (Opposite.op j)).f' ≫ ((Functor.const J).obj X).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ c.ι.app ⊥ ≫ l = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
j : J
⊢ c.ι.app j ≫ l ≫ p = c.ι.app j ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
⊢ sq.HasLift

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
j✝ j'✝ : { x // x ∈ Set.Iio j }ᵒᵖ
f : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom ((⋯.functor.op ⋙ F).map f))
      ((fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val)
        j✝) =
    (fun x ↦
        match x with
        | op ⟨i, hi⟩ => (e i hi).val)
      j'✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (F.map (homOfLE ⋯)) p
f✝ : F.obj ⊥ ⟶ X
g✝ : ((Functor.const J).obj c.pt).obj ⊥ ⟶ Y
sq : CommSq f✝ (c.ι.app ⊥) p g✝
j : J
hj : ¬IsMax j
x✝¹ : F.obj j ⟶ X
x✝ : CommSq x✝¹ (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g✝)
⊢ x✝.HasLift

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ⊥ < j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.llp.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    val₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ i < Order.succ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ (coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ ((coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} W ≤ W.rlp.llp

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
by

Goal state after: