mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case ofNat
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.ofNat a✝).log = Int.ofNat a✝ • x.log

pp: case negSucc
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.negSucc a✝).log = Int.negSucc a✝ • x.log

Tactic:
<;>

Goal state after:
case ofNat
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.ofNat a✝).log = Int.ofNat a✝ • x.log

case negSucc
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.negSucc a✝).log = Int.negSucc a✝ • x.log
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top.top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

pp: case top.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤

pp: case coe.top
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

pp: case coe.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤

Tactic:
<;>

Goal state after:
case top.top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

case top.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤

case coe.top
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

case coe.coe
G : Type u_1
inst✝ : AddCommGroup G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
⊢ ⊤ - b = ⊤ + -b

pp: case coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
a✝ : G
⊢ ↑a✝ - b = ↑a✝ + -b

Tactic:
<;>

Goal state after:
case top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
⊢ ⊤ - b = ⊤ + -b

case coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
b : WithTop G
a✝ : G
⊢ ↑a✝ - b = ↑a✝ + -b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
⊢ ⊤ - ⊤ = ⊤ + -⊤

pp: case top.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ + -↑a✝

pp: case coe.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ↑a✝ - ⊤ = ↑a✝ + -⊤

pp: case coe.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ↑a✝¹ + -↑a✝

Tactic:
<;>

Goal state after:
case top.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
⊢ ⊤ - ⊤ = ⊤ + -⊤

case top.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤ + -↑a✝

case coe.top
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝ : G
⊢ ↑a✝ - ⊤ = ↑a✝ + -⊤

case coe.coe
G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a✝¹ a✝ : G
⊢ ↑a✝¹ - ↑a✝ = ↑a✝¹ + -↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
⊢ 1 ≤ ⊤

pp: case coe
α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
a✝ : α
⊢ 1 ≤ ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
⊢ 1 ≤ ⊤

case coe
α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
a✝ : α
⊢ 1 ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤

pp: case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤

case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

pp: case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

pp: case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤

pp: case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤

Tactic:
<;>

Goal state after:
case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤

case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ y ≠ ⊤

pp: case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ y ≠ ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ y ≠ ⊤

case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ y ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊤

pp: case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ↑a✝ ≠ ⊤

pp: case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ ⊤ ≠ ⊤

pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ ≠ ⊤ ↔ ↑a✝¹ ≠ ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
<;>

Goal state after:
case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊤

case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ↑a✝ ≠ ⊤

case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ ⊤ ≠ ⊤

case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ ≠ ⊤ ↔ ↑a✝¹ ≠ ⊤ ∧ ↑a✝ ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) none → none = none

pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
c : α
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) (Option.some c) → none = Option.some c

pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) none → Option.some b = none

pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) (Option.some c) → Option.some b = Option.some c

Tactic:
<;>

Goal state after:
case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) none → none = none

case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
c : α
⊢ (fun x ↦ ↑a + x) none = (fun x ↦ ↑a + x) (Option.some c) → none = Option.some c

case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) none → Option.some b = none

case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ (fun x ↦ ↑a + x) (Option.some b) = (fun x ↦ ↑a + x) (Option.some c) → Option.some b = Option.some c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) none → none = none

pp: case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
c : α
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) (Option.some c) → none = Option.some c

pp: case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) none → Option.some b = none

pp: case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) (Option.some c) → Option.some b = Option.some c

Tactic:
<;>

Goal state after:
case none.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) none → none = none

case none.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
c : α
⊢ (fun x ↦ x + ↑a) none = (fun x ↦ x + ↑a) (Option.some c) → none = Option.some c

case some.none
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) none → Option.some b = none

case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ (fun x ↦ x + ↑a) (Option.some b) = (fun x ↦ x + ↑a) (Option.some c) → Option.some b = Option.some c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ y) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ y) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)

pp: case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)

Tactic:
<;>

Goal state after:
case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) ((fun x1 x2 ↦ x1 + x2) ⊤ z)

case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ y) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ y) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) y) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

pp: case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)

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

Tactic:
<;>

Goal state after:
case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ⊤) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

case top.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ⊤ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) ⊤ z)

case coe.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ⊤ z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝ ⊤) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝) z)

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) (↑a✝) z →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) (swap (fun x1 x2 ↦ x1 + x2) (↑a✝¹) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊤ y) ((fun x1 x2 ↦ x1 + x2) ⊤ z) → (fun x1 x2 ↦ x1 < x2) y z

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

Tactic:
<;>

Goal state after:
case top
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊤ y) ((fun x1 x2 ↦ x1 + x2) ⊤ z) → (fun x1 x2 ↦ x1 < x2) y z

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z) → (fun x1 x2 ↦ x1 < x2) y z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ z) → (fun x1 x2 ↦ x1 < x2) ⊤ z

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

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

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

Tactic:
<;>

Goal state after:
case top.top
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithTop α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ⊤ ⊤) ((fun x1 x2 ↦ x1 + x2) ⊤ z) → (fun x1 x2 ↦ x1 < x2) ⊤ z

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

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

case coe.coe
α : Type u
β : Type v
inst✝² : Add α
w x y z✝ : WithTop α
a b : α
inst✝¹ : LT α
inst✝ : AddLeftReflectLT α
z : WithTop α
a✝¹ a✝ : α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x1 x2 ↦ x1 + x2) ↑a✝¹ ↑a✝) ((fun x1 x2 ↦ x1 + x2) (↑a✝¹) z) →
    (fun x1 x2 ↦ x1 < x2) (↑a✝) z
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

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

Tactic:
<;>

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

Goal state before:
pp: case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊤ ≤ ↑x + z → ⊤ ≤ z

pp: case coe
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + z → ↑a✝ ≤ z

Tactic:
<;>

Goal state after:
case top
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + ⊤ ≤ ↑x + z → ⊤ ≤ z

case coe
α : Type u
inst✝² : Add α
z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝ : α
⊢ ↑x + ↑a✝ ≤ ↑x + z → ↑a✝ ≤ z