awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
X Y : C
f : X ⟶ Y
⊢ P.retracts f → P f
have mp : ∀ (w w_1 : C) (w_2 : w ⟶ w_1) (h₂ : RetractArrow f w_2) (h₃ : P w_2), P f
Tactic: ⟨_, _, _, h₂, h₃⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q ↔ P ≤ Q
have mp : P.retracts ≤ Q → P ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Retract (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
mp : P.retracts ≤ Q → P ≤ Q
⊢ P.retracts ≤ Q ↔ P ≤ Q
have mpr : P ≤ Q → P.retracts ≤ Q
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.RetractArgument (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
inst_1 : W₁.HasFactorization W₂
inst_2 : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
⊢ W₁ i
have have : ∀ (h : W₁.MapFactorizationData W₂ i), W₁ i
Tactic: have h := factorizationData W₁ W₂ i
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.RetractArgument (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
inst_1 : W₁.HasFactorization W₂
inst_2 : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
⊢ W₁ i
have this : HasLiftingProperty i (h.p (W₁ := W₁) (W₂ := W₂))
Tactic: have := hi _ h.hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.RetractArgument (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
inst_1 : W₁.HasFactorization W₂
inst_2 : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
⊢ W₂ p
have have : ∀ (h : W₁.MapFactorizationData W₂ p), W₂ p
Tactic: have h := factorizationData W₁ W₂ p
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.RetractArgument (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty.{v_1, u_1} C
inst_1 : W₁.HasFactorization W₂
inst_2 : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
⊢ W₂ p
have this : HasLiftingProperty (h.i (W₁ := W₁) (W₂ := W₂)) p
Tactic: have := hp _ h.hi
-- 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'_1 : Type w'
inst_6 : LinearOrder J'_1
inst_7 : SuccOrder J'_1
inst_8 : OrderBot J'_1
inst_9 : WellFoundedLT J'_1
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst_10 : LinearOrder J'
inst_11 : OrderBot J'
inst_12 : SuccOrder J'
inst_13 : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
⊢ W (Y :=
    (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
    ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).map (homOfLE ⋯))
have have : ∀
  (this :
    W (X := h.toTransfiniteCompositionOfShape (W := W).F.obj ((e : (a : J') → J) j)) (Y :=
      h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ ((e : (a : J') → J) j)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))),
  W (Y :=
    (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
    ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).map (homOfLE sorry))
Tactic: have := h.map_mem (e j) (by simpa only [e.isMax_apply])
-- 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'_1 : Type w'
inst_6 : LinearOrder J'_1
inst_7 : SuccOrder J'_1
inst_8 : OrderBot J'_1
inst_9 : WellFoundedLT J'_1
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst_10 : LinearOrder J'
inst_11 : OrderBot J'
inst_12 : SuccOrder J'
inst_13 : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
this :
  W (X := h.toTransfiniteCompositionOfShape (W := W).F.obj ((e : (a : J') → J) j)) (Y :=
    h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ ((e : (a : J') → J) j)))
    (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (Y :=
    (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
    ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).map (homOfLE ⋯))
have rw : ∀
  (this :
    Arrow.mk (X := h.toTransfiniteCompositionOfShape (W := W).F.obj ((e : (a : J') → J) j)) (Y :=
        h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ ((e : (a : J') → J) j)))
        (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry)) ∈
      W.toSet),
  Arrow.mk (Y :=
      (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
      ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).map (homOfLE sorry)) ∈
    W.toSet
Tactic: rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
Cleared hypotheses: this
-- 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'_1 : Type w'
inst_6 : LinearOrder J'_1
inst_7 : SuccOrder J'_1
inst_8 : OrderBot J'_1
inst_9 : WellFoundedLT J'_1
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst_10 : LinearOrder J'
inst_11 : OrderBot J'
inst_12 : SuccOrder J'
inst_13 : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
this :
  Arrow.mk (X := h.toTransfiniteCompositionOfShape (W := W).F.obj ((e : (a : J') → J) j)) (Y :=
      h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ ((e : (a : J') → J) j)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet
eq :
  Arrow.mk (Y := (e : (a : J') → J) (Order.succ j)) (homOfLE ⋯) =
    Arrow.mk (X := (e : (a : J') → J) j) (Y := Order.succ ((e : (a : J') → J) j)) (homOfLE ⋯)
⊢ Arrow.mk (Y :=
      (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
      ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).map (homOfLE ⋯)) ∈
    W.toSet
have eq₁ : h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
    (Arrow.mk (Y := (e : (a : J') → J) (Order.succ j)) (homOfLE sorry)) =
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
    (Arrow.mk (X := (e : (a : J') → J) j) (Y := Order.succ ((e : (a : J') → J) j)) (homOfLE sorry))
Tactic: replace eq := congr_arg h.F.mapArrow.obj eq
Cleared hypotheses: eq
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ¬IsMax i
⊢ ¬IsMax (↑i : J)
have rw : ∀ (hi : ∃ (b : (↑(Set.Iic j) : Type w)), i < b), ∃ (b : J), (↑i : J) < b
Tactic: rw [not_isMax_iff] at hi ⊢
Cleared hypotheses: hi
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ∃ (b : (↑(Set.Iic j) : Type w)), i < b
⊢ ∃ (b : J), (↑i : J) < b
have obtain : ∀ (i' : (↑(Set.Iic j) : Type w)) (hi' : i < i'), ∃ (b : J), (↑i : J) < b
Tactic: obtain ⟨i', hi'⟩ := hi
Cleared hypotheses: hi
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ¬IsMax i
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE ⋯))
have have : ∀
  (this :
    W (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))),
  W (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE sorry))
Tactic: have := h.map_mem i.1 (by
      rw [not_isMax_iff] at hi ⊢
      obtain ⟨i', hi'⟩ := hi
      exact ⟨j, lt_of_lt_of_le hi' i'.2⟩)
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ¬IsMax i
this :
  W (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
    (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE ⋯))
have rw : ∀
  (this :
    Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
        (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry)) ∈
      W.toSet),
  Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE sorry)) ∈
    W.toSet
Tactic: rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
Cleared hypotheses: this
-- 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'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ¬IsMax i
this :
  Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet
⊢ Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq : Arrow.mk (X := Functor.obj (Monotone.functor sorry) i) (Y := Functor.obj (Monotone.functor sorry) (Order.succ i))
    (Functor.map (Monotone.functor sorry) (homOfLE sorry)) =
  Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE sorry)
Tactic: have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (Set.Iic.coe_succ_of_not_isMax hi) 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'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Iic j) : Type w)
hi : ¬IsMax i
this :
  Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet
eq :
  Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
      (Functor.map (Monotone.functor ⋯) (homOfLE ⋯)) =
    Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯)
⊢ Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq₁ : h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
    (Arrow.mk (X := Functor.obj (Monotone.functor sorry) i) (Y := Functor.obj (Monotone.functor sorry) (Order.succ i))
      (Functor.map (Monotone.functor sorry) (homOfLE sorry))) =
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE sorry))
Tactic: replace eq := congr_arg h.F.mapArrow.obj eq
Cleared hypotheses: eq
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Ici j) : Type w)
hi : ¬IsMax i
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯))
have have : ∀
  (this :
    W (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry))),
  W (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE sorry))
Tactic: have := h.map_mem i.1 (Set.not_isMax_coe _ hi)
-- 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
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Ici j) : Type w)
hi : ¬IsMax i
this :
  W (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
    (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯))
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯))
have rw : ∀
  (this :
    Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
        (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE sorry)) ∈
      W.toSet),
  Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE sorry)) ∈
    W.toSet
Tactic: rw [← W.arrow_mk_mem_toSet_iff] at this ⊢
Cleared hypotheses: this
-- 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'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Ici j) : Type w)
hi : ¬IsMax i
this :
  Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet
⊢ Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq : Arrow.mk (X := Functor.obj (Monotone.functor sorry) i) (Y := Functor.obj (Monotone.functor sorry) (Order.succ i))
    (Functor.map (Monotone.functor sorry) (homOfLE sorry)) =
  Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE sorry)
Tactic: have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (coe_succ_of_mem (i.2.trans (Order.le_succ _))) 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'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : (↑(Set.Ici j) : Type w)
hi : ¬IsMax i
this :
  Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet
eq :
  Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
      (Functor.map (Monotone.functor ⋯) (homOfLE ⋯)) =
    Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯)
⊢ Arrow.mk (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯)) ∈
    W.toSet
have eq₁ : h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
    (Arrow.mk (X := Functor.obj (Monotone.functor sorry) i) (Y := Functor.obj (Monotone.functor sorry) (Order.succ i))
      (Functor.map (Monotone.functor sorry) (homOfLE sorry))) =
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE sorry))
Tactic: replace eq := congr_arg h.F.mapArrow.obj eq
Cleared hypotheses: eq
-- 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'
n : ℕ
F : ComposableArrows.{v, u} C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
j : Fin (n + 1)
hj : ¬IsMax j
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
have inl : ∀ (j : Fin n) (hj : ¬IsMax j.castSucc),
  W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE sorry))
Tactic: obtain ⟨j, rfl⟩ | rfl := j.eq_castSucc_or_eq_last
Cleared hypotheses: j, 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'
n : ℕ
F : ComposableArrows.{v, u} C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
j : Fin (n + 1)
hj : ¬IsMax j
inl :
  ∀ (j : Fin n) (hj : ¬IsMax j.castSucc),
    W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
      ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
have inr : ∀ (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 sorry))
Tactic: obtain ⟨j, rfl⟩ | rfl := j.eq_castSucc_or_eq_last
Cleared hypotheses: j, 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'
n : ℕ
F : ComposableArrows.{v, u} C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
j : Fin n
hj : ¬IsMax j.castSucc
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
have inl : ∀ (hF : W (F.map (homOfLE sorry))),
  W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE sorry))
Tactic: replace hF := hF j
Cleared hypotheses: hF
-- 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'
n : ℕ
F : ComposableArrows.{v, u} C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : W (F.map (homOfLE ⋯))
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))
have inl : ∀ (hF : Arrow.mk (F.map (homOfLE sorry)) ∈ W.toSet),
  Arrow.mk (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
      ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE sorry)) ∈
    W.toSet
Tactic: rw [← W.arrow_mk_mem_toSet_iff] at hF ⊢
Cleared hypotheses: hF