Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) → (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

pp: case bot.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

pp: case bot.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

pp: case bot.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

pp: case coe.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

pp: case coe.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

pp: case coe.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

pp: case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) → (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

case bot.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

case bot.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

case bot.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ⊥ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝

case coe.bot.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ⊥

case coe.bot.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ⊥ ↑a✝

case coe.coe.bot
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ⊥) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝ ⊥

case coe.coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z : WithBot α
a b : α
inst✝¹ : LT α
inst✝ : AddRightReflectLT α
a✝² a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝¹) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝² ↑a✝) →
    (fun x1 x2 ↦ x1 < x2) ↑a✝¹ ↑a✝