mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case zero.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

pp: case zero.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

pp: case succ.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

pp: case succ.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
a✝ : α
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

Tactic:
<;>

Goal state after:
case zero.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

case zero.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝

case succ.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
⊢ (match ⊤, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ⊤, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ⊤

case succ.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n n✝ : ℕ
a✝ : α
⊢ (match ↑a✝, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match ↑a✝, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
a✝ : α
⊢ ↑a✝ ^ n = ⊤ ↔ ↑a✝ = ⊤ ∧ n ≠ 0

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
a✝ : α
⊢ ↑a✝ ^ n = ⊤ ↔ ↑a✝ = ⊤ ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊤ ^ 0 = ⊤ ↔ ⊤ = ⊤ ∧ 0 ≠ 0

pp: case top.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n✝ : ℕ
⊢ ⊤ ^ (n✝ + 1) = ⊤ ↔ ⊤ = ⊤ ∧ n✝ + 1 ≠ 0

pp: case coe.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
⊢ ↑a✝ ^ 0 = ⊤ ↔ ↑a✝ = ⊤ ∧ 0 ≠ 0

pp: case coe.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
n✝ : ℕ
⊢ ↑a✝ ^ (n✝ + 1) = ⊤ ↔ ↑a✝ = ⊤ ∧ n✝ + 1 ≠ 0

Tactic:
<;>

Goal state after:
case top.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊤ ^ 0 = ⊤ ↔ ⊤ = ⊤ ∧ 0 ≠ 0

case top.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n✝ : ℕ
⊢ ⊤ ^ (n✝ + 1) = ⊤ ↔ ⊤ = ⊤ ∧ n✝ + 1 ≠ 0

case coe.zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
⊢ ↑a✝ ^ 0 = ⊤ ↔ ↑a✝ = ⊤ ∧ 0 ≠ 0

case coe.succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a✝ : α
n✝ : ℕ
⊢ ↑a✝ ^ (n✝ + 1) = ⊤ ↔ ↑a✝ = ⊤ ∧ n✝ + 1 ≠ 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + b) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind b fun b ↦ Option.some (c * b)

pp: case neg.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + b) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind b fun b ↦ Option.some (c * b)

Tactic:
<;>

Goal state after:
case neg.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + b) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind b fun b ↦ Option.some (c * b)

case neg.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + b) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind b fun b ↦ Option.some (c * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

pp: case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

pp: case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

pp: case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

Tactic:
<;>

Goal state after:
case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ⊤ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)

case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝ fun b ↦ Option.some (c * b)) + Option.bind ⊤ fun b ↦ Option.some (c * b)

case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun b ↦ Option.some (c * b)) =
    (Option.bind ↑a✝¹ fun b ↦ Option.some (c * b)) + Option.bind ↑a✝ fun b ↦ Option.some (c * b)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + b) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind b fun a ↦ Option.some (a * c)

pp: case neg.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + b) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind b fun a ↦ Option.some (a * c)

Tactic:
<;>

Goal state after:
case neg.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + b) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind b fun a ↦ Option.some (a * c)

case neg.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
b : WithTop α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + b) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind b fun a ↦ Option.some (a * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

pp: case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

pp: case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

pp: case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝¹ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

Tactic:
<;>

Goal state after:
case neg.top.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
⊢ (Option.bind (⊤ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

case neg.top.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (⊤ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ⊤ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)

case neg.coe.top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝ : α
⊢ (Option.bind (↑a✝ + ⊤) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝ fun a ↦ Option.some (a * c)) + Option.bind ⊤ fun a ↦ Option.some (a * c)

case neg.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c : α
hc : ¬c = 0
a✝¹ a✝ : α
⊢ (Option.bind (↑a✝¹ + ↑a✝) fun a ↦ Option.some (a * c)) =
    (Option.bind ↑a✝¹ fun a ↦ Option.some (a * c)) + Option.bind ↑a✝ fun a ↦ Option.some (a * c)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  0 < n + 1 →
    (∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)) → x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1

pp: case succ.succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  0 < n + 1 →
    (∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)) → x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1

Tactic:
<;>

Goal state after:
case succ.succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  0 < n + 1 →
    (∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)) → x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1

case succ.succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  0 < n + 1 →
    (∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)) → x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
k : ℕ
hk : k < n + 1
⊢ k < n + 1 + 1
Module: Mathlib.Order.Iterate

Goal state before:
pp: case h₀
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x

pp: case hx
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)

pp: case hy
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x

Tactic:
<;>

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x

case hx
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)

case hy
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
⊢ ⊥ * b = if ⊥ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ b

pp: case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
a✝ : α
⊢ ↑a✝ * b = if ↑a✝ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) (↑a✝) b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
⊢ ⊥ * b = if ⊥ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ b

case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
a✝ : α
⊢ ↑a✝ * b = if ↑a✝ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) (↑a✝) b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊥ * ⊥ = if ⊥ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ⊥

pp: case bot.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊥ * ↑a✝ = if ⊥ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ↑a✝

pp: case coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊥ = if ↑a✝ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊥

pp: case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊥ * ⊥ = if ⊥ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ⊥

case bot.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊥ * ↑a✝ = if ⊥ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊥ ↑a✝

case coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊥ = if ↑a✝ = 0 ∨ ⊥ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊥

case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
⊢ Contravariant { x // 0 < x } (WithBot α) (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro ⟨x, x0⟩ a b h
    simp only at h
    lift x to α using x0.ne_bot
    cases a
    · exact bot_le
    cases b
    · rw [bot_mul x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_ge
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact le_of_mul_le_mul_right h x0

Goal state after:
Module: Mathlib.Order.SuccPred.WithBot

Goal state before:
pp: case top
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
⊢ ⊤.pred = ⊤ ↔ ⊤ = ⊤

pp: case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
⊢ (↑a✝).pred = ⊤ ↔ ↑a✝ = ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
⊢ ⊤.pred = ⊤ ↔ ⊤ = ⊤

case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
⊢ (↑a✝).pred = ⊤ ↔ ↑a✝ = ⊤
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩
  rw [hb.Iio_eq] at ha
  obtain rfl := isLUB_Iic.unique ha
  cases hb.lt.false

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
⊢ StrictMonoOn f s

Tactic:
rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab.le
  obtain _ | n := n
  · simp at hab
  apply not_isMax_of_lt at hab
  induction n with
  | zero => simpa using hf _ hab ha hb
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n + 1] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

Goal state after: