mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this✝ : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
this : transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ ¬IsMax j₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
⊢ ∃ j, transfiniteIterate φ j i₀ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
⊢ L.map T₁'.mor₁ ≫ e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂ = (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ L.map T₂'.mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ G.Additive ↔ (L ⋙ G).Additive

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
⊢ HasCardinalLT X κ ↔ Cardinal.mk X < κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
⊢ Small.{v, u} X

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
κ' : Cardinal.{v}
hκ' : κ ≤ κ'
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ'

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ HasCardinalLT Y κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ HasCardinalLT Y κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
⊢ HasCardinalLT X Cardinal.aleph0 ↔ Finite X

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
inst✝ : Finite X
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X Cardinal.aleph0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
q : W.LeftFraction w₁.Y' w₂.Y'
fac₃ : z₂.s ≫ w₂.s ≫ q.s = z₁.s ≫ w₁.s ≫ q.f
⊢ a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type v
κ : Cardinal.{w}
⊢ HasCardinalLT X (Cardinal.lift.{u, w} κ) ↔ HasCardinalLT X κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ F.map (L.map (f - g)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ L.map f = L.map g

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{max w u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, w} κ
⊢ Cardinal.aleph0 ≤ Cardinal.lift.{max u' u, w} κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (Option X) κ ↔ HasCardinalLT X κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
a : α
⊢ (P.limitsClosure J).limitsOfShape (J a) ≤ P.limitsClosure J

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
⊢ HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : ∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)
h : P ≤ Q
⊢ P.limitsClosure J ≤ Q

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
⊢ HasCardinalLT (Subtype (P₁ ⊔ P₂)) κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure.limitsClosure J = P.limitsClosure J

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ Cardinal.lift.{w, w} (Cardinal.mk ι) < κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
⊢ HasCardinalLT (ULift.{max v w, u} ι) (Cardinal.lift.{max u v, w} κ)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
i : ULift.{max v w, u} ι
⊢ HasCardinalLT (ULift.{max u w, v} (α i.down)) (Cardinal.lift.{max u v, w} κ)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
h : P ≤ Q
⊢ P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ
x✝ : (i : ι) × Subtype (P i)
i : ι
x : X
hx : P i x
⊢ (⨆ i, P i) x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨i, ⟨x, hx⟩⟩ => ⟨x, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT (↑(S i)) κ
⊢ HasCardinalLT (↑(⋃ i, S i)) κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ Cardinal.aleph0 ≤ Cardinal.lift.{max u u', w} κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (ULift.{max u' w, u} T₁) (Cardinal.lift.{max u u', w} κ)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
inst✝ : Small.{w, u} X
⊢ HasCardinalLT X (Order.succ (max (Cardinal.mk (Shrink.{w, u} X)) Cardinal.aleph0))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type v
X : ι → Type u
inst✝¹ : Small.{w, v} ι
inst✝ : ∀ (i : ι), Small.{w, u} (X i)
⊢ ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
⊢ P.strictLimitsClosureIter J b ≤ P.limitsClosure J

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹⁰ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁹ : LinearOrder β
inst✝⁸ : OrderBot β
inst✝⁷ : SuccOrder β
inst✝⁶ : WellFoundedLT β
inst✝⁵ : ObjectProperty.Small.{w, v, u} P
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : Small.{w, t} α
inst✝² : ∀ (a : α), Small.{w, u'} (J a)
inst✝¹ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
b✝ : β
hb₀ : Small.{w, w'} ↑(Set.Iio b✝)
b c : β
hbc : b ≤ c
inst✝ : Small.{w, w'} ↑(Set.Iio c)
x✝² x✝¹ : ↑(Set.Iio b)
x✝ : (fun x ↦ ⟨↑x, ⋯⟩) x✝² = (fun x ↦ ⟨↑x, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
c : ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
b : β
hb₀ : Small.{w, w'} ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
⊢ ∃ m, ∃ (_ : m < κ.ord), ∀ (j : J a), o j ≤ m

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
a : α
⊢ (P.colimitsClosure J).colimitsOfShape (J a) ≤ P.colimitsClosure J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
⊢ a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : ∀ (a : α), Q.IsClosedUnderColimitsOfShape (J a)
h : P ≤ Q
⊢ P.colimitsClosure J ≤ Q

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ ¬IsMax m

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure.colimitsClosure J = P.colimitsClosure J

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.colimitsClosure J = (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁵ : (a : α) → Category.{v', u'} (J a)
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure J)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
a : α
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a) ≤
    (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
a : α
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure.limitsOfShape (J a) ≤ (P.strictLimitsClosureIter J κ.ord).isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
⊢ (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
Q : ObjectProperty C
hQ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (Q.isoClosure.limitsClosure J)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁶ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝⁵ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

Tactic:
by

Goal state after: