mathlib-initiative/mathlib-tactics huggingface dataset:
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
X Y : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
⊢ add W eX' eY' f₁ f₂ = add W eX' eY' f₁ f₂

Tactic:
]

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 ≫ z₁.f ≫ w₁.s

Tactic:
]

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
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)

Tactic:
]

Goal state after:
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
X Y : C
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_3
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map (β.s ≫ γ.s) = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)

Tactic:
]

Goal state after:
case refine_3
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map (β.s ≫ γ.s) = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_3
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map β.s ≫ L.map γ.s = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)

Tactic:
]

Goal state after:
case refine_3
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ β.map L ⋯ ≫ L.map β.s ≫ L.map γ.s = ψ.thd.map L ⋯ ≫ L.map (β.s ≫ γ.s)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_3
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.s ≫ γ.s = α.s ≫ γ.f
ψ : W.LeftFraction₃ X Y := { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, f'' := β.f ≫ γ.s, s := β.s ≫ γ.s, hs := ⋯ }
this : IsIso (L.map (β.s ≫ γ.s))
⊢ L.map β.f ≫ L.map γ.s = L.map β.f ≫ L.map γ.s

Tactic:
]

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

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
W : MorphismProperty C
inst✝² : L.IsLocalization W
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ L.map φ.fst.f = L.map φ.snd.f

Tactic:
]

Goal state after:
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
W : MorphismProperty C
inst✝² : L.IsLocalization W
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
φ : W.LeftFraction₂ X₁ X₂
hfg : F.map (φ.fst.map L ⋯) = F.map (φ.snd.map L ⋯)
⊢ L.map φ.fst.f = L.map φ.snd.f
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
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
]

Goal state after:
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
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) fun y x h ↦ ⨆ x, h ↑x ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀)

Tactic:
]

Goal state after:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) fun y x h ↦ ⨆ x, h ↑x ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀)
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ (⨆ x,
        (fun x x_1 ↦
            SuccOrder.limitRecOn x (motive := fun x ↦ I → I) (fun x x_2 ↦ id) (fun x x_2 g ↦ φ ∘ g) fun y x h ↦
              ⨆ x, h ↑x ⋯)
          ↑x ⋯)
      i₀ =
    ⨆ x,
      SuccOrder.limitRecOn ↑x (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀

Tactic:
]

Goal state after:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : Order.IsSuccLimit j
⊢ (⨆ x,
        (fun x x_1 ↦
            SuccOrder.limitRecOn x (motive := fun x ↦ I → I) (fun x x_2 ↦ id) (fun x x_2 g ↦ φ ∘ g) fun y x h ↦
              ⨆ x, h ↑x ⋯)
          ↑x ⋯)
      i₀ =
    ⨆ x,
      SuccOrder.limitRecOn ↑x (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isMin
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
k✝ k : J
hk : IsMin k
hkj : k✝ ≤ k
⊢ (fun j ↦ transfiniteIterate φ j i₀) k✝ ≤ (fun j ↦ transfiniteIterate φ j i₀) k

Tactic:
obtain rfl := hk.eq_bot
    obtain rfl : k = ⊥ := by simpa using hkj
    rfl

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ.inl
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
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)

Tactic:
]

Goal state after:
case succ.inl
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
k k' : J
hk' : ¬IsMax k'
hkk' : k ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj✝ : k ≤ Order.succ k'
hkj : k < Order.succ k'
⊢ transfiniteIterate φ k' i₀ ≤ φ (transfiniteIterate φ k' i₀)
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
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv

Tactic:
]

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isSuccLimit.inl
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
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) b
hkj✝ : k ≤ k'
hkj : k < k'
⊢ transfiniteIterate φ k i₀ ≤ ⨆ x, transfiniteIterate φ (↑x) i₀

Tactic:
]

Goal state after:
case isSuccLimit.inl
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
k k' : J
hk' : Order.IsSuccLimit k'
a✝ : ∀ b < k', k ≤ b → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) b
hkj✝ : k ≤ k'
hkj : k < k'
⊢ transfiniteIterate φ k i₀ ≤ ⨆ x, transfiniteIterate φ (↑x) i₀
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case pos
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₀
⊢ ⊤ ≤ ⊤

Tactic:
]

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₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀

Tactic:
]

Goal state after:
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₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mpr
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
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (L.map φ.f) + G.map (L.map φ.f') = G.map (L.map φ.fst.f) + G.map (L.map φ.snd.f)

Tactic:
]

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.s = a₂.s ≫ t₂ ≫ w₂.f ≫ q.s

Tactic:
]

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

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

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

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : Finite X
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
⊢ Finite X
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 - g) = 0

Tactic:
]

Goal state after:
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 - g) = 0
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: case mpr
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.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
]

Goal state after:
case mpr
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.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
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)
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case mpr
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.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
]

Goal state after:
case mpr
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.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ Finite PUnit.{1}

Tactic:
]

Goal state after:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
x✝ : HasCardinalLT X κ
⊢ Finite PUnit.{1}
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₁) κ ∧ HasCardinalLT (Subtype P₂) κ

Tactic:
]

Goal state after:
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₁) κ ∧ HasCardinalLT (Subtype P₂) κ