mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ 0 ≤ b

Tactic:
cases b

Goal state after:
case zero.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ 0 ≤ ↑a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ ↑a✝ ≤ b

Tactic:
cases b

Goal state after:
case coe.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝¹ a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝¹ ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ 0 ≤ b

Tactic:
cases b

Goal state after:
case zero.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ 0 ≤ ↑a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ ↑a✝ ≤ b

Tactic:
cases b

Goal state after:
case coe.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝¹ ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂

Tactic:
mk'_eq_iff_eq_mul,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f.mk' x₂ y₂ * f ↑y₁
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
n : ℕ
ih : (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
⊢ r /ₒ s * (r /ₒ s) ^ n = r * r ^ n /ₒ (s ^ n * s)

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
n : ℕ
ih : (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
⊢ r /ₒ s * (r ^ n /ₒ s ^ n) = r * r ^ n /ₒ (s ^ n * s)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk (x * ↑y) (1 * y) = mk x 1

Tactic:
conv =>

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
| mk (x * 1) (1 * 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
cases b

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

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

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

Tactic:
cases b

Goal state after:
case coe.top
α : 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.Ring.Equiv

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S'✝ : Type u_6
inst✝⁶ : NonUnitalNonAssocSemiring R✝
inst✝⁵ : NonUnitalNonAssocSemiring S✝
f✝ : R✝ ≃+* S✝
x : R✝
inst✝⁴ : FunLike F R✝ S✝
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring R'
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x✝¹ x✝ : R × S
⊢ ((↑f).prodCongr ↑g).toFun (x✝¹ * x✝) = ((↑f).prodCongr ↑g).toFun x✝¹ * ((↑f).prodCongr ↑g).toFun x✝

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_mul, Prod.mk_mul_mk]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
cases b

Goal state after:
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹² : Monoid M
S : Submonoid M
inst✝¹¹ : OreSet S
inst✝¹⁰ : MulAction M X
inst✝⁹ : SMul R X
inst✝⁸ : SMul R M
inst✝⁷ : IsScalarTower R M M
inst✝⁶ : IsScalarTower R M X
inst✝⁵ : SMul R' X
inst✝⁴ : SMul R' M
inst✝³ : IsScalarTower R' M M
inst✝² : IsScalarTower R' M X
inst✝¹ : SMul R R'
inst✝ : IsScalarTower R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (r • m) • x = r • m • x

Tactic:
rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul,
      ← mul_smul, mul_div_one]
    simp only [smul_mul_assoc, smul_assoc, one_mul]

Goal state after:
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)

Tactic:
cases b

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)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
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:
cases b

Goal state after:
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 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)

Tactic:
cases b

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)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
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:
cases b

Goal state after:
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.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

Tactic:
cases b

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✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
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:
cases b

Goal state after:
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: 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

Tactic:
cases b

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

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✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: 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

Tactic:
cases b

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

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

Goal state before:
pp: 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

Tactic:
cases b

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

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

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

Tactic:
cases b

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

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✝
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
cases b

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

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
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
cases b

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

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✝
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
cases b

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

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✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: 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

Tactic:
cases b

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

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

Goal state before:
pp: 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

Tactic:
cases b

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

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
⊢ (∀ (i : α), i ≠ ⊥ → P i) ↔ ∀ (i : α), P (succ i)

Tactic:
by
  refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩
  obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)
  have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]
  rw [← Nat.succ_pred_eq_of_pos hj]
  simp only [Function.iterate_succ', Function.comp_apply]
  apply h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
← lt_succ_iff_of_not_isMax hb,

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a < succ b
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: m n a b : ℕ
h : a < b
⊢ a ≤ b.pred

Tactic:
cases b

Goal state after:
case zero
m n a : ℕ
h : a < 0
⊢ a ≤ pred 0

case succ
m n a n✝ : ℕ
h : a < n✝ + 1
⊢ a ≤ (n✝ + 1).pred
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ a < succ b ↔ b = a ∨ a < b

Tactic:
rw [eq_comm, lt_succ_iff_eq_or_lt]

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

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

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✝
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: 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)

Tactic:
cases b

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

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

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

Tactic:
cases b

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

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

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

Tactic:
cases b

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

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

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

Tactic:
cases b

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

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

Goal state before:
pp: a b : ℕ∞
h : a < b
⊢ a ≤ b - 1

Tactic:
cases b

Goal state after:
case top
a : ℕ∞
h : a < ⊤
⊢ a ≤ ⊤ - 1

case coe
a : ℕ∞
a✝ : ℕ
h : a < ↑a✝
⊢ a ≤ ↑a✝ - 1
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(succ a) = succ ↑a

Tactic:
classical
  change Subtype.val (dite ..) = _
  split_ifs <;> trivial

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem ha]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ f a * ∏ x ∈ s \ {a}, f x