awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₄ : ¬k₂ < j
isSuccLimit : ∀ (h₁₂ : k₁ ≤ j) (h₃ : j ≤ j) (h₄ : ¬j < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃

Tactic:
obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃

Premises used: le_antisymm, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
⊢ restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯

Tactic:
have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
pos : ∀ (h₅ : k₁ < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
neg : ∀ (h₅ : ¬k₁ < j), MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

Tactic:
by_cases h₅ : k₁ < j
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : k₁ < j
pos : arrowι (restrictionLT iter₁.F h₃) h₁ k₁ h₅ = arrowι (restrictionLT iter₂.F h₃) h₁ k₁ h₅
⊢ arrowMap iter₁.F k₁ j h₁₂ h₃ = arrowMap iter₂.F k₁ j h₁₂ h₃

Tactic:
simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < j
⊢ j ≤ k₁

Tactic:
simpa using h₅
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this_1 : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j) (h₄ : k₂ < j), MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < j
neg :
  ∀ (h₁ : Order.IsSuccLimit k₁) (h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F)
    (iter₁ iter₂ : Φ.Iteration k₁)
    (this : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁) (h₄ : k₂ < k₁), MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃)
    (h₁₂ h₃ : k₁ ≤ k₁) (h₄ : ¬k₁ < k₁) (this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯) (h₅ : ¬k₁ < k₁),
    MapEq iter₁.F iter₂.F k₁ k₁ h₁₂ h₃
⊢ MapEq iter₁.F iter₂.F k₁ j h₁₂ h₃

Tactic:
obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)

Premises used: le_antisymm, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j k₁ : J
h₁ : Order.IsSuccLimit k₁
h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration k₁
this_1 : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁) (h₄ : k₂ < k₁), MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃
h₁₂ h₃ : k₁ ≤ k₁
h₄ : ¬k₁ < k₁
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < k₁
neg :
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃)
⊢ MapEq iter₁.F iter₂.F k₁ k₁ h₁₂ h₃

Tactic:
apply mapEq_refl

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_refl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j k₁ : J
h₁ : Order.IsSuccLimit k₁
h₂ : ∀ b < k₁, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration k₁
this_1 : ∀ (k₁_1 k₂ : J) (h₁₂ : k₁_1 ≤ k₂) (h₃ : k₂ ≤ k₁) (h₄ : k₂ < k₁), MapEq iter₁.F iter₂.F k₁_1 k₂ h₁₂ h₃
h₁₂ h₃ : k₁ ≤ k₁
h₄ : ¬k₁ < k₁
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : ¬k₁ < k₁
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k₁) k₁ h₃)

Tactic:
simp only [obj_limit _ _ h₁, this]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
isMin : ∀ (j : J) (h : IsMin j) (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
succ :
  ∀ (j : J) (hj₁ : ¬IsMax j) (hj₂ : ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F)
    (iter₁ iter₂ : Φ.Iteration (Order.succ j)), iter₁.F = iter₂.F
isSuccLimit :
  ∀ (j : J) (h₁ : Order.IsSuccLimit j) (h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F)
    (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F
⊢ ∀ (iter₁ iter₂ : Φ.Iteration j), iter₁.F = iter₂.F

Tactic:
induction j using SuccOrder.limitRecOn with
    | isMin j h =>
      obtain rfl := h.eq_bot
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      obtain rfl : k₂ = ⊥ := by simpa using h₂
      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
      apply mapEq_refl _ _ (by simp only [obj_bot])
    | succ j hj₁ hj₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
      have h₀ := Order.le_succ j
      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
      dsimp at hj₂ hsucc
      wlog h : k₂ ≤ j generalizing k₁ k₂
      · obtain h₂ | rfl := h₂.lt_or_eq
        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
        · by_cases h' : k₁ ≤ j
          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
              arrowSucc_eq, hsucc]
          · simp only [not_le] at h'
            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
            rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]
      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
    | isSuccLimit j h₁ h₂ =>
      intro iter₁ iter₂
      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
        simp at this
        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
        by_cases h₅ : k₁ < j
        · dsimp [MapEq]
          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
          apply mapEq_refl
          simp only [obj_limit _ _ h₁, this]

Premises used: not_le, Order.succ, CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.ext, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.mapEq_refl, CategoryTheory.SmallObject.SuccStruct.succ, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
inr :
  ∀
    (this :
      ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
        iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
          iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂))
    (h : ¬j₁ ≤ j₂),
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
wlog :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)

Tactic:
wlog h : j₁ ≤ j₂ generalizing j₁ j₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
h : ¬j₁ ≤ j₂
⊢ j₂ < j₁

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k : J
h₁ : k ≤ j₁
h₂ : k ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) (h : j₁ ≤ j₂),
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
h : ¬j₁ ≤ j₂
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)

Tactic:
exact (this iter₂ iter₁ h₂ h₁ (le_of_lt (by simpa using h))).symm

Premises used: le_of_lt, Eq.symm
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
rw :
  (iter₂.trunc h).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)
⊢ iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)

Tactic:
rw [Subsingleton.elim iter₁ (iter₂.trunc h)]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.trunc, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
⊢ (iter₂.trunc h).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k h₂)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
inr :
  ∀
    (this :
      ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
        arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂)
    (hj : ¬j₁ ≤ j₂), arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
wlog :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
    arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∀ {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂),
    arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
hj : ¬j₁ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k₁ k₂ : J
h : k₁ ≤ k₂
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
rw : arrowMap (iter₂.trunc hj).F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
rw [Subsingleton.elim iter₁ (iter₂.trunc hj)]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.trunc, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k₁ k₂ : J
h : k₁ ≤ k₂
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ arrowMap (iter₂.trunc hj).F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ ∃ (hX :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ ⋯) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ ⋯))
    (hY :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
    iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯

Tactic:
have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂)
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∃ (hX :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ ⋯) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ ⋯))
    (hY :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
    iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
tauto tauto₁ tauto₂ :
  ∀
    (w :
      iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ ⋯) =
        iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ ⋯))
    (w_1 :
      iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
        iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
    iter₁.F.map (homOfLE h) = eqToHom w ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯ →
      iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ Arrow.mk (iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj) = arrowMap iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
simp [mapObj, arrowMap]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj, CategoryTheory.SmallObject.SuccStruct.arrowMap
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j_1 j : J
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ j ≤ j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j : J
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ iter.mapObj iter h ⋯ h' ⋯ = iter.F.map (homOfLE h)

Tactic:
simp [mapObj]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ j₃ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
iter₃ : Φ.Iteration j₃
k₁ k₂ k₃ : J
h₁₂ : k₁ ≤ k₂
h₂₃ : k₂ ≤ k₃
h₁ : k₁ ≤ j₁
h₂ : k₂ ≤ j₂
h₃ : k₃ ≤ j₃
h₁₂' : j₁ ≤ j₂
h₂₃' : j₂ ≤ j₃
⊢ iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂' ≫ iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃' = iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯

Tactic:
simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map, CategoryTheory.Functor.map_comp, LE.le.trans
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
⊢ j ∈ Set.Iic j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
i : (↑(Set.Iic j) : Type u)
⊢ obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (↑i : J) ⋯) = F.obj i

Tactic:
dif_pos i.2

Premises used: Set.Mem, setOf, dif_pos, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj, Set.Iic, Subtype.property
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ Order.succ j ∈ Set.Iic (Order.succ j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
⊢ ¬(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯) : J) ≤ j

Tactic:
simpa only [Order.succ_le_iff_isMax] using hj

Premises used: Order.succ_le_iff_isMax
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : i₁ ≤ j
e_i : Order.succ j = i₂
⊢ obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯) =
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ hi₂)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : i₁ ≤ j
⊢ Order.succ j = i₂

Tactic:
le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂

Premises used: not_le, Order.succ_le_of_lt, le_antisymm, Iff.mp