awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
n : ℕ
F : ComposableArrows.{v, u} C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet
⊢ Arrow.mk (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
      ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq : Arrow.mk (Y := Order.succ j.castSucc) (homOfLE sorry) = Arrow.mk (homOfLE sorry)
Tactic: have eq : Arrow.mk (homOfLE (Order.le_succ j.castSucc)) =
        Arrow.mk (homOfLE j.castSucc_le_succ) :=
          Arrow.ext rfl j.orderSucc_castSucc rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
n : ℕ
F : ComposableArrows.{v, u} C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (Y := Order.succ j.castSucc) (homOfLE ⋯) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
      ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq₁ : (Functor.mapArrow F).obj (Arrow.mk (Y := Order.succ j.castSucc) (homOfLE sorry)) =
  (Functor.mapArrow F).obj (Arrow.mk (homOfLE sorry))
Tactic: replace eq := congr_arg F.mapArrow.obj eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
n : ℕ
F : ComposableArrows.{v, u} C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬IsMax (Fin.last n)
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ (Fin.last n)))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
have hj₁ : ¬Fin.last n = ⊤
Tactic: rw [isMax_iff_eq_top] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
X Y : C
f : X ⟶ Y
hf : W f
i : Fin 1
⊢ W ((ComposableArrows.mk₁ f).map (homOfLE ⋯))
have 0 : W (X := (ComposableArrows.mk₁ f).obj (Fin.castSucc ((fun (i : Fin 1) ↦ i) ⟨0, sorry⟩)))
  ((ComposableArrows.mk₁ f).map (homOfLE sorry))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
i : Fin 2
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))
have 0 : W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)))
  ((ComposableArrows.mk₂ f g).map (homOfLE sorry))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
J : Type w
inst_2 : LinearOrder J
inst_3 : SuccOrder J
inst_4 : OrderBot J
inst_5 : WellFoundedLT J
J' : Type w'
inst_6 : LinearOrder J'
inst_7 : SuccOrder J'
inst_8 : OrderBot J'
inst_9 : WellFoundedLT J'
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : W f
hg : W g
i : Fin 2
0 :
  W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)))
    ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))
have 1 : W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)))
  ((ComposableArrows.mk₂ f g).map (homOfLE sorry))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
J' : Type w'
inst_5 : LinearOrder J'
inst_6 : SuccOrder J'
inst_7 : OrderBot J'
inst_8 : WellFoundedLT J'
e : J ≃o J'
⊢ W.transfiniteCompositionsOfShape J = W.transfiniteCompositionsOfShape J'
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W.transfiniteCompositionsOfShape J f ↔ W.transfiniteCompositionsOfShape J' f
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
⊢ W (hf.toTransfiniteCompositionOfShape (W := W).F.map g)
have obtain : W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y := hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
  (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: obtain rfl : g = homOfLE bot_le := rfl
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : IsMin j
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
have isMin : ∀ (hj : IsMin.{w} (α := J) ⊥),
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: obtain rfl := hj.eq_bot
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' :
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
have succ : W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
  hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
  (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry) ≫
    hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
have isMin : ∀ (j : J) (hj : IsMin j),
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    letI : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
isMin :
  ∀ (j : J) (hj : IsMin j),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
have succ : ∀ (j : J) (hj : ¬IsMax j)
  (hj' :
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))),
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
    (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    letI : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst_5 : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst_6 : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
isMin :
  ∀ (j : J) (hj : IsMin j),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
succ :
  ∀ (j : J) (hj : ¬IsMax j)
    (hj' :
      W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
        hf.toTransfiniteCompositionOfShape (W := W).F.obj j)
        (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))),
    W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
      hf.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ j))
      (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
have isSuccLimit : ∀ (j : J) (hj : Order.IsSuccLimit j)
  (hj' :
    ∀ b < j,
      W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
        hf.toTransfiniteCompositionOfShape (W := W).F.obj b)
        (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))),
  W (X := hf.toTransfiniteCompositionOfShape (W := W).F.obj ⊥) (Y :=
    hf.toTransfiniteCompositionOfShape (W := W).F.obj j) (hf.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    letI : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
inst_2 : UnivLE.{w, w'}
J : Type w
x : LinearOrder J
x_1 : SuccOrder J
x_2 : OrderBot J
h : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape J
have rw : IsStableUnderTransfiniteCompositionOfShape.{w', v, u} W (Shrink.{w', w} J)
Tactic: rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
      (orderIsoShrink.{w'} J)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f
have rw : ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
  W.transfiniteCompositionsOfShape J f
Tactic: rw [transfiniteCompositions_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W₁ f
⊢ transfiniteCompositions.{w, v, u} W₂ f
have hf₁ : ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
  W₁.transfiniteCompositionsOfShape J f
Tactic: rw [transfiniteCompositions_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W₁.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W₂ f
have obtain : ∀ (J : Type w) (w : LinearOrder J) (w_1 : SuccOrder J) (w_2 : OrderBot J) (w_3 : WellFoundedLT J)
  (hf : W₁.transfiniteCompositionsOfShape J f), transfiniteCompositions.{w, v, u} W₂ f
Tactic: obtain ⟨J, _, _, _, _, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W f
⊢ W f
have hf₁ : ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
  W.transfiniteCompositionsOfShape J f
Tactic: rw [transfiniteCompositions_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.IsStableUnderTransfiniteComposition
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f
⊢ W f
have obtain : ∀ (J : Type w) (w : LinearOrder J) (w_1 : SuccOrder J) (w_2 : OrderBot J) (w_3 : WellFoundedLT J)
  (hf : W.transfiniteCompositionsOfShape J f), W f
Tactic: obtain ⟨J, _, _, _, _, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q
have mp : transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderTransfiniteComposition
mp : transfiniteCompositions.{w, v, u} P ≤ Q → P ≤ Q
⊢ transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q
have mpr : P ≤ Q → transfiniteCompositions.{w, v, u} P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.NatIso (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f
have h : Eq.{v₂ + 1} (α := G.obj X ⟶ F.obj Y)
  ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) ((app X).hom ≫ G.map f))
  ((fun (f : F.obj X ⟶ G.obj Y) ↦ (app X).inv ≫ f ≫ (app Y).inv) (F.map f ≫ (app Y).hom))
Tactic: have h := congr_arg (fun f => (app X).inv ≫ f ≫ (app Y).inv) (naturality f).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.NatIso (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
⊢ (ofComponents app' @naturality).app X = app' X
have w : ((ofComponents app' @naturality).app X).hom = (app' X).hom
Tactic: cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.NatIso (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)
have revert : ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
Tactic: revert F₁ F₂
Cleared hypotheses: F₁, F₂, e
-- Lean 4 proof step from Mathlib.CategoryTheory.NatIso (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
have suffices : ∀ {F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D} (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)
Tactic: suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
    fun F₁ F₂ e => ⟨this e, this e.symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ ofObj.{v, u, u'} X Y ↔ ∃ (i : ι), X i = Y
have mp : ofObj.{v, u, u'} X Y → ∃ (i : ι), X i = Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
mp : ofObj.{v, u, u'} X Y → ∃ (i : ι), X i = Y
⊢ ofObj.{v, u, u'} X Y ↔ ∃ (i : ι), X i = Y
have mpr : (∃ (i : ι), X i = Y) → ofObj.{v, u, u'} X Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
P : ObjectProperty.{v, u} C
⊢ ofObj (ι := Subtype P) (Subtype.val (p := P)) = P
have h : ∀ (X : C), ofObj.{v, u, u} (ι := Subtype P) (Subtype.val (p := P)) X ↔ P X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair.{v, u} X Y Z ↔ X = Z ∨ Y = Z
have mp : pair.{v, u} X Y Z → X = Z ∨ Y = Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y Z : C
mp : pair.{v, u} X Y Z → X = Z ∨ Y = Z
⊢ pair.{v, u} X Y Z ↔ X = Z ∨ Y = Z
have mpr : X = Z ∨ Y = Z → pair.{v, u} X Y Z
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
val : Unit
⊢ X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val) ∨
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val)
have mp : ¬X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val) →
  Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inl val)
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
X Y : C
val : Unit
⊢ X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val) ∨
    Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val)
have mp : ¬X = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val) →
  Y = Sum.elim (fun (x : Unit) ↦ X) (fun (x : Unit) ↦ Y) (Sum.inr val)
Tactic: tauto
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
ι : Type u'
X : ι → C
F : Functor.{v, v', u, u'} C D
⊢ strictMap (ofObj X) F = ofObj (F.obj ∘ X)
have h : ∀ (Y : D), strictMap (ofObj X) F Y ↔ ofObj.{v', u', u'} (F.obj ∘ X) Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Basic (goal)
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
X : C
F : Functor.{v, v', u, u'} C D
⊢ strictMap (singleton X) F = singleton (F.obj X)
have h : ∀ (x : D), strictMap (singleton X) F x ↔ singleton.{v', u'} (F.obj X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure = P
have a : P.isoClosure ≤ P
Tactic: apply le_antisymm