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

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n✝ : ℕ
⊢ (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:
cases a

Goal state after:
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 neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (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:
cases a

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
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (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:
cases a

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: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b

Tactic:
cases a

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 pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 ↑0 = unbotD 0 ↑0 * unbotD 0 b

Tactic:
unbotD_coe,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ 0 = 0 * unbotD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 ↑0 = unbotD 0 a * unbotD 0 ↑0

Tactic:
unbotD_coe,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ 0 = unbotD 0 a * 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
cases a

Goal state after:
case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ unbotD 0 ↑(a✝¹ * a✝) = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝

Tactic:
unbotD_coe,

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝

Tactic:
unbotD_coe,

Goal state after:
case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ a✝¹ * a✝ = a✝¹ * unbotD 0 ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
⊢ ↑x * a ≤ ↑x * b

Tactic:
cases a

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b

case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ b
⊢ ↑x * ↑a✝ ≤ ↑x * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
⊢ a * ↑x ≤ b * ↑x

Tactic:
cases a

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x

case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ b
⊢ ↑a✝ * ↑x ≤ b * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ ↑x * a < ↑x * ↑a✝

Tactic:
cases a

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝

case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑x * ↑a✝ < ↑x * ↑a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ a * ↑x < ↑a✝ * ↑x

Tactic:
cases a

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑a✝ * ↑x < ↑a✝¹ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * a < ↑x * ↑a✝
⊢ a < ↑a✝

Tactic:
cases a

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * ⊥ < ↑x * ↑a✝
⊢ ⊥ < ↑a✝

case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑x * ↑a✝ < ↑x * ↑a✝¹
⊢ ↑a✝ < ↑a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : a * ↑x < ↑a✝ * ↑x
⊢ a < ↑a✝

Tactic:
cases a

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ⊥ * ↑x < ↑a✝ * ↑x
⊢ ⊥ < ↑a✝

case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝ * ↑x < ↑a✝¹ * ↑x
⊢ ↑a✝ < ↑a✝¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
a b : WithBot α
x : α
x0 : 0 < ↑x
h : ↑x * a ≤ ↑x * b
⊢ a ≤ b

Tactic:
cases a

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ↑x * ⊥ ≤ ↑x * b
⊢ ⊥ ≤ b

case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑x * ↑a✝ ≤ ↑x * b
⊢ ↑a✝ ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
a b : WithBot α
x : α
x0 : 0 < ↑x
h : a * ↑x ≤ b * ↑x
⊢ a ≤ b

Tactic:
cases a

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ⊥ * ↑x ≤ b * ↑x
⊢ ⊥ ≤ b

case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ b * ↑x
⊢ ↑a✝ ≤ b
Module: Mathlib.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
⊢ a.succ = ⊥ ↔ a = ⊥

Tactic:
cases a

Goal state after:
case bot
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
⊢ ⊥.succ = ⊥ ↔ ⊥ = ⊥

case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥
Module: Mathlib.Order.SuccPred.WithBot

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

Tactic:
cases a

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 b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
rw [← not_iff_not]
  simp [h.le_iff_forall_le]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)

Tactic:
← Nat.succ_pred_eq_of_pos hj

Goal state after:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j.pred.succ] ⊥)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m

Tactic:
refine (hm x hx).resolve_left ?_

Goal state after:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ ¬x = succ m
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a : ℕ
ha : a ≤ a.pred
⊢ IsMin a

Tactic:
cases a

Goal state after:
case zero
m n : ℕ
ha : 0 ≤ pred 0
⊢ IsMin 0

case succ
m n n✝ : ℕ
ha : n✝ + 1 ≤ (n✝ + 1).pred
⊢ IsMin (n✝ + 1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ y - 1 ↔ x < y

Tactic:
← pred_eq_sub_one,

Goal state after:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ pred y ↔ x < y
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))

Tactic:
induction n generalizing a with

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : WithBot α
⊢ a.succ = 0 ↔ a = ⊥

Tactic:
cases a

Goal state after:
case bot
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
⊢ ⊥.succ = 0 ↔ ⊥ = ⊥

case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a✝ : α
⊢ (↑a✝).succ = 0 ↔ ↑a✝ = ⊥
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ x - 1 < y ↔ x ≤ y

Tactic:
← pred_eq_sub_one,

Goal state after:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ pred x < y ↔ x ≤ y
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    a
⊢ IsMax a

Tactic:
cases a

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
ha :
  (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ⊤
⊢ IsMax ⊤

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha :
  (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝
⊢ IsMax ↑a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : succ a✝ ≤ a✝
⊢ IsMax ↑a✝

Tactic:
succ_le_iff_isMax,

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : IsMax a✝
⊢ IsMax ↑a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
a✝ : α
h : a < ↑a✝
⊢ (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝

Tactic:
cases a

Goal state after:
case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
h : ⊤ < ↑a✝
⊢ (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ (match ↑a✝ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ↑a✝¹
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f (a - 1) < f a) → StrictMono f

Tactic:
by
  simpa [Order.pred_eq_sub_one] using strictMono_of_pred_lt (f := f)

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b

Tactic:
simpa using h₂

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e :
  (fun a ↦ ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) a =
    (fun a ↦ ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) b
⊢ a = b

Tactic:
by
      dsimp at e
      injection e with h₁ h₂
      simpa using h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a b : WithTop α
h : a < b
⊢ (match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    b

Tactic:
cases b
    · exact le_top
    cases a
    · exact (not_top_lt h).elim
    rw [coe_lt_coe] at h
    change ite _ _ _ ≤ _
    split_ifs with ha
    · rw [succ_eq_iff_isMax] at ha
      exact (ha.not_lt h).elim
    · exact coe_le_coe.2 (succ_le_of_lt h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha :
  a ≤
    match a with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin a

Tactic:
cases a

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha :
  ⊤ ≤
    match ⊤ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ⊤

case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha :
  ↑a✝ ≤
    match ↑a✝ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ↑a✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a b : WithTop α
h : a < b
⊢ a ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)

Tactic:
cases a

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
b : WithTop α
h : ⊤ < b
⊢ ⊤ ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)

case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
b : WithTop α
a✝ : α
h : ↑a✝ < b
⊢ ↑a✝ ≤
    match b with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b : ℕ∞
⊢ (a * b).toNat = a.toNat * b.toNat

Tactic:
cases a

Goal state after:
case top
b : ℕ∞
⊢ (⊤ * b).toNat = ⊤.toNat * b.toNat

case coe
b : ℕ∞
a✝ : ℕ
⊢ (↑a✝ * b).toNat = (↑a✝).toNat * b.toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top.coe
b : ℕ
⊢ (⊤ * ↑b).toNat = ⊤.toNat * (↑b).toNat

Tactic:
cases b <;> simp

Goal state after:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.top
a : ℕ
⊢ (↑a * ⊤).toNat = (↑a).toNat * ⊤.toNat

Tactic:
cases a

Goal state after:
case coe.top.zero
⊢ (↑0 * ⊤).toNat = (↑0).toNat * ⊤.toNat

case coe.top.succ
n✝ : ℕ
⊢ (↑(n✝ + 1) * ⊤).toNat = (↑(n✝ + 1)).toNat * ⊤.toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
⊢ motive a

Tactic:
cases a

Goal state after:
case top
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
⊢ motive ⊤

case coe
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
a✝ : ℕ
⊢ motive ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
a b : ℕ∞
e : (fun x ↦ x + n) a = (fun x ↦ x + n) b
⊢ a = b

Tactic:
exact le_antisymm
    ((WithTop.add_le_add_iff_right hn).mp e.le)
    ((WithTop.add_le_add_iff_right hn).mp e.ge)

Goal state after:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ
n : WithTop ℕ∞
h : ↑m < n
⊢ ↑(m + 1) ≤ n

Tactic:
match n with
  | ⊤ => exact le_top
  | (⊤ : ℕ∞) => exact WithTop.coe_le_coe.2 (OrderTop.le_top _)
  | (n : ℕ) => simpa only [Nat.cast_le, ge_iff_le, Nat.cast_lt] using! h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
⊢ j ∈ s → Function.update f i b j = f j

Tactic:
hj

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∉ s
f : ι → M
b : M
j : ι
hj : j ∈ s
⊢ Function.update f i b j = f j
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : Uncountable β
⊢ Uncountable (α × β)

Tactic:
inhabit α
  exact (Prod.mk_right_injective default).uncountable

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ (Sym.cast ⋯) (s.append (replicate (↑i) b)) ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
mem_cast,

Goal state after:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ s.append (replicate (↑i) b) ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s