-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma congr_arrowMap {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
    {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) :
    arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

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

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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₂

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Tactic:
wlog hj : j₁ ≤ j₂ generalizing j₁ j₂

Result:
case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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₂),
    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₂

C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂

Proof state:
case inr
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : 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₂),
    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)]

Result:
no goals