awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯)
⊢ h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯))

Tactic:
replace eq := congr_arg h.F.mapArrow.obj eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯))
⊢ Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet

Tactic:
this
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (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

Tactic:
convert! this using 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
have :
  ∀
    (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 ⋯))
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem i.1 (Set.not_isMax_coe _ hi)
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯))
rw :
  ∀
    (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
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).ici j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).ici j).F.map (homOfLE ⋯))

Tactic:
rw [← W.arrow_mk_mem_toSet_iff] at this ⊢

Premises used: CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 (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 ⋯)

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
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯)
⊢ h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯))

Tactic:
replace eq := congr_arg h.F.mapArrow.obj eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (Arrow.mk (Y := Order.succ (↑i : J)) (homOfLE ⋯))
⊢ Arrow.mk (Y := h.toTransfiniteCompositionOfShape (W := W).F.obj (Order.succ (↑i : J)))
      (h.toTransfiniteCompositionOfShape (W := W).F.map (homOfLE ⋯)) ∈
    W.toSet

Tactic:
this
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := Functor.obj (Monotone.functor ⋯) i) (Y := Functor.obj (Monotone.functor ⋯) (Order.succ i))
        (Functor.map (Monotone.functor ⋯) (homOfLE ⋯))) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj (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

Tactic:
convert! this using 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯))
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 ⋯))
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
obtain ⟨j, rfl⟩ | rfl := j.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
inl :
  ∀ (hF : W (F.map (homOfLE ⋯))),
    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.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
replace hF := hF j
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯))
inl :
  ∀ (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
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ j.castSucc))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
rw [← W.arrow_mk_mem_toSet_iff] at hF ⊢

Premises used: CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 := Order.succ j.castSucc) (homOfLE ⋯) = Arrow.mk (homOfLE ⋯)

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
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯)
⊢ (Functor.mapArrow F).obj (Arrow.mk (Y := Order.succ j.castSucc) (homOfLE ⋯)) =
    (Functor.mapArrow F).obj (Arrow.mk (homOfLE ⋯))

Tactic:
replace eq := congr_arg F.mapArrow.obj eq
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  (Functor.mapArrow F).obj (Arrow.mk (Y := Order.succ j.castSucc) (homOfLE ⋯)) =
    (Functor.mapArrow F).obj (Arrow.mk (homOfLE ⋯))
⊢ Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
hF
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 :
  (Functor.mapArrow F).obj (Arrow.mk (Y := Order.succ j.castSucc) (homOfLE ⋯)) =
    (Functor.mapArrow F).obj (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

Tactic:
convert! hF using 1
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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)
⊢ ¬Fin.last n = ⊤

Tactic:
rw [isMax_iff_eq_top] at hj

Premises used: isMax_iff_eq_top
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 : ¬Fin.last n = ⊤
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ (Fin.last n)))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
(hj rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 : ¬Fin.last n = ⊤
⊢ W (Y := (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.obj (Order.succ (Fin.last n)))
    ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
exact (hj rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 : C
⊢ ∀ (i : Fin 0),
    W (X := Functor.obj.{0, v, 0, u} (ComposableArrows.mk₀ X) i.castSucc)
      (Functor.map (ComposableArrows.mk₀ X) (homOfLE ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
0 :
  W (X := (ComposableArrows.mk₁ f).obj (Fin.castSucc ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩)))
    ((ComposableArrows.mk₁ f).map (homOfLE ⋯))
⊢ W ((ComposableArrows.mk₁ f).map (homOfLE ⋯))

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
⊢ W (X := (ComposableArrows.mk₁ f).obj (Fin.castSucc ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩)))
    ((ComposableArrows.mk₁ f).map (homOfLE ⋯))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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 ⋯))
1 :
  W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)))
    ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))
⊢ W ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
⊢ W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)))
    ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
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
⊢ W (X := (ComposableArrows.mk₂ f g).obj (Fin.castSucc ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)))
    ((ComposableArrows.mk₂ f g).map (homOfLE ⋯))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
t : a.TransfiniteCompositionOfShape J f
⊢ b.transfiniteCompositionsOfShape J f

Tactic:
⟨t.ofLE h⟩

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape, Nonempty.intro, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofLE
-- Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
a b : MorphismProperty.{v, u} C
h : a ≤ b
X Y : C
f : X ⟶ Y
t : a.TransfiniteCompositionOfShape J f
⊢ b.transfiniteCompositionsOfShape J f

Tactic:
exact ⟨t.ofLE h⟩