-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem cmp_veblenWith :
  cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | .eq => cmp a b
    | .lt => cmp a (veblenWith f o₂ b)
    | .gt => cmp (veblenWith f o₁ a) b

Proof state:
case inr.inl
f : Ordinal.{u} → Ordinal.{u}
o₁ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₁ b) =
    match cmp o₁ o₁ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₁ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
simp [(veblenWith_right_strictMono hf _).cmp_map_eq]

Result:
no goals

Proof state:
case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inl
f : Ordinal.{u} → Ordinal.{u}
o₁ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₁ b) =
    match cmp o₁ o₁ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₁ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
on_goal 2 => simp [(veblenWith_right_strictMono hf _).cmp_map_eq]

Result:
case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Proof state:
case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
all_goals
  conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
  simp [h.cmp_eq_lt, h.cmp_eq_gt, h.ne, h.ne', (veblenWith_right_strictMono hf _).cmp_map_eq]

Result:
no goals

Proof state:
case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]

Result:
case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
obtain h | rfl | h := lt_trichotomy o₁ o₂

Result:
case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inl
f : Ordinal.{u} → Ordinal.{u}
o₁ a b : Ordinal.{u}
hf : IsNormal f
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₁ b) =
    match cmp o₁ o₁ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₁ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Proof state:
case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
simp [h.cmp_eq_lt, h.cmp_eq_gt, h.ne, h.ne', (veblenWith_right_strictMono hf _).cmp_map_eq]

Result:
no goals