awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
w w_1 : C
w_2 : w ⟶ w_1
h₂ : RetractArrow f w_2
h₃ : P w_2
⊢ P f

Tactic:
h₁ h₂ h₃
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
w w_1 : C
w_2 : w ⟶ w_1
h₂ : RetractArrow f w_2
h₃ : P w_2
⊢ P f

Tactic:
exact h₁ h₂ h₃
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
mpr : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X : C
mpr : ∀ {Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y : C
mpr : ∀ {Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y Z : C
mpr : ∀ {W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y Z W : C
mpr : ∀ {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y Z W : C
f : X ⟶ Y
mpr : ∀ {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f
⊢ ∀ {g : Z ⟶ W} (h : RetractArrow f g) (hg : P g), P f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h₂ : RetractArrow f g
h₃ : P g
⊢ P f

Tactic:
h₁ _ ⟨_, _, _, h₂, h₃⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
h₁ : P.retracts ≤ P
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h₂ : RetractArrow f g
h₃ : P g
⊢ P f

Tactic:
exact h₁ _ ⟨_, _, _, h₂, h₃⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 rwa rwa₁ rwa₂ rwa₃ : P.IsStableUnderRetracts
⊢ P.retracts ≤ P

Tactic:
rwa [← isStableUnderRetracts_iff_retracts_le]

Premises used: CategoryTheory.MorphismProperty.isStableUnderRetracts_iff_retracts_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
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
mpr : P ≤ Q → P.retracts ≤ Q
⊢ P.retracts ≤ Q ↔ P ≤ Q

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q → P ≤ Q

Tactic:
le_trans P.le_retracts

Premises used: CategoryTheory.MorphismProperty.le_retracts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
⊢ P.retracts ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_retracts

Premises used: CategoryTheory.MorphismProperty.le_retracts, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ P.retracts ≤ Q

Tactic:
le_trans (retracts_monotone h) Q.retracts_le

Premises used: CategoryTheory.MorphismProperty.retracts_le, CategoryTheory.MorphismProperty.retracts_monotone, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : Q.IsStableUnderRetracts
h : P ≤ Q
⊢ P.retracts ≤ Q

Tactic:
exact le_trans (retracts_monotone h) Q.retracts_le

Premises used: CategoryTheory.MorphismProperty.retracts_le, CategoryTheory.MorphismProperty.retracts_monotone, le_trans
-- Module: Mathlib.CategoryTheory.MorphismProperty.Retract
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderRetracts
⊢ P.RespectsIso

Tactic:
RespectsIso.of_respects_arrow_iso _
    (fun _ _ e ↦ of_retract (Retract.ofIso e.symm))

Premises used: CategoryTheory.Retract.ofIso, CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso, CategoryTheory.Iso.symm, CategoryTheory.MorphismProperty.of_retract
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst_1 : HasLiftingProperty f p
⊢ i ≫ p = f ≫ 𝟙 Z

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
i : X ⟶ Y
p : Y ⟶ Z
h : i ≫ p = f
inst_1 : HasLiftingProperty i f
⊢ 𝟙 X ≫ f = i ≫ p

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
have : ∀ (h : W₁.MapFactorizationData W₂ i), W₁ i
⊢ W₁ i

Tactic:
have h := factorizationData W₁ W₂ i
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
⊢ HasLiftingProperty i (h.p (W₁ := W₁) (W₂ := W₂))

Tactic:
have := hi _ h.hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
this : HasLiftingProperty i (h.p (W₁ := W₁) (W₂ := W₂))
⊢ W₁ i

Tactic:
simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.fac, CategoryTheory.MorphismProperty.of_retract, CategoryTheory.MorphismProperty.MapFactorizationData.hi, CategoryTheory.RetractArrow.ofLeftLiftingProperty
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
have : ∀ (h : W₁.MapFactorizationData W₂ p), W₂ p
⊢ W₂ p

Tactic:
have h := factorizationData W₁ W₂ p
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
⊢ HasLiftingProperty (h.i (W₁ := W₁) (W₂ := W₂)) p

Tactic:
have := hp _ h.hi
-- Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument
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
this : HasLiftingProperty (h.i (W₁ := W₁) (W₂ := W₂)) p
⊢ W₂ p

Tactic:
simpa using of_retract (RetractArrow.ofRightLiftingProperty h.fac) h.hp

Premises used: CategoryTheory.RetractArrow.ofRightLiftingProperty, CategoryTheory.MorphismProperty.MapFactorizationData.fac, CategoryTheory.MorphismProperty.of_retract, CategoryTheory.MorphismProperty.MapFactorizationData.hp
-- 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'_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
⊢ ¬IsMax.{w} (α := J) ((e : (a : J') → J) j : J)

Tactic:
simpa only [e.isMax_apply]

Premises used: OrderIso.isMax_apply
-- 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'_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
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 ⋯))),
    W (Y :=
      (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
      ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).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 ⋯))

Tactic:
have := h.map_mem (e j) (by simpa only [e.isMax_apply])
-- 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'_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 ⋯))
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 ⋯)) ∈
        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 ⋯)) ∈
      W.toSet
⊢ W (Y :=
    (TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).obj (Order.succ j))
    ((TransfiniteCompositionOfShape.F (h.toTransfiniteCompositionOfShape (W := W).ofOrderIso e)).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'_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 ⋯)
⊢ h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (Y := (e : (a : J') → J) (Order.succ j)) (homOfLE ⋯)) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := (e : (a : J') → J) j) (Y := Order.succ ((e : (a : J') → J) 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'_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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (Y := (e : (a : J') → J) (Order.succ j)) (homOfLE ⋯)) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (X := (e : (a : J') → J) j) (Y := Order.succ ((e : (a : J') → J) j)) (homOfLE ⋯))
⊢ 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

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'_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 :
  h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (Arrow.mk (Y := (e : (a : J') → J) (Order.succ j)) (homOfLE ⋯)) =
    h.toTransfiniteCompositionOfShape (W := W).F.mapArrow.obj
      (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

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.Iic j) : Type w)
hi : ¬IsMax i
rw : ∀ (hi : ∃ (b : (↑(Set.Iic j) : Type w)), i < b), ∃ (b : J), (↑i : J) < b
⊢ ¬IsMax (↑i : J)

Tactic:
rw [not_isMax_iff] at hi ⊢

Premises used: not_isMax_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.Iic j) : Type w)
hi : ∃ (b : (↑(Set.Iic j) : Type w)), i < b
obtain : ∀ (i' : (↑(Set.Iic j) : Type w)) (hi' : i < i'), ∃ (b : J), (↑i : J) < b
⊢ ∃ (b : J), (↑i : J) < b

Tactic:
obtain ⟨i', hi'⟩ := 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 i' : (↑(Set.Iic j) : Type w)
hi' : i < i'
⊢ ∃ (b : J), (↑i : J) < b

Tactic:
⟨j, lt_of_lt_of_le hi' i'.2⟩

Premises used: Exists.intro, lt_of_lt_of_le, Subtype.property
-- 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 i' : (↑(Set.Iic j) : Type w)
hi' : i < i'
⊢ ∃ (b : J), (↑i : J) < b

Tactic:
exact ⟨j, lt_of_lt_of_le hi' i'.2⟩
-- 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
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).iic j).F.obj (Order.succ i))
      ((h.toTransfiniteCompositionOfShape (W := W).iic j).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 ⋯))

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⟩)
-- 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 :
  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).iic j).F.obj (Order.succ i))
        ((h.toTransfiniteCompositionOfShape (W := W).iic j).F.map (homOfLE ⋯)) ∈
      W.toSet
⊢ W (Y := (h.toTransfiniteCompositionOfShape (W := W).iic j).F.obj (Order.succ i))
    ((h.toTransfiniteCompositionOfShape (W := W).iic 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.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 (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 (Set.Iic.coe_succ_of_not_isMax hi) rfl