awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
top₁ : HPow.hPow (β := ℕ∞) (1 * y) ⊤ = HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ * HPow.hPow (β := ℕ∞) y ⊤
top₂ : ∀ (x_2 : 1 < x), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_0 : x < 1
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
simp only [lt_one_iff_eq_zero.1 x_0, zero_mul, zero_epow_top]

Premises used: MulZeroClass.zero_mul, Iff.mp, ENat.zero_epow_top, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y z : ℕ∞
⊢ HPow.hPow (β := ℕ∞) (1 * y) ⊤ = HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
simp only [one_mul, one_epow]

Premises used: one_mul, ENat.one_epow
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
top : ∀ (y_0 : y < 1), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
top₁ : HPow.hPow (β := ℕ∞) (x * 1) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤
top₂ : ∀ (y_2 : 1 < y), HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
rcases lt_trichotomy y 1 with y_0 | rfl | y_2

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
y_0 : y < 1
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
simp only [lt_one_iff_eq_zero.1 y_0, mul_zero, zero_epow_top]

Premises used: MulZeroClass.mul_zero, Iff.mp, ENat.zero_epow_top, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x z : ℕ∞
x_2 : 1 < x
⊢ HPow.hPow (β := ℕ∞) (x * 1) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤

Tactic:
simp
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
top : HPow.hPow (β := ℕ∞) (x * y) ⊤ = ⊤
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤

Tactic:
rw [epow_top x_2, epow_top y_2, WithTop.top_mul_top]

Premises used: WithTop.top_mul_top, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = ⊤

Tactic:
epow_top (one_lt_mul x_2.le y_2)

Premises used: LT.lt.le, one_lt_mul, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ HPow.hPow (β := ℕ∞) (x * y) ⊤ = ⊤

Tactic:
exact epow_top (one_lt_mul x_2.le y_2)

Premises used: LT.lt.le, one_lt_mul, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
a : ℕ
⊢ HPow.hPow (β := ℕ∞) (x * y) (↑a : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) y (↑a : ℕ∞)

Tactic:
simp only [epow_natCast, mul_pow x y]

Premises used: ENat.epow_natCast, mul_pow
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
inl : ∀ (y_0 : y = 0), x ^ (y * z) = (x ^ y) ^ z
inr : ∀ (y_0 : y ≠ 0), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases eq_or_ne y 0 with y_0 | y_0

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
simp [y_0]
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
inr : ∀ (z_0 : z = 0), x ^ (y * z) = (x ^ y) ^ z
inr₁ : ∀ (z_0 : z ≠ 0), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases eq_or_ne z 0 with z_0 | z_0

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z = 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
simp [z_0]
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
inr : ∀ (x_0 : x < 1), x ^ (y * z) = (x ^ y) ^ z
inr₁ : HPow.hPow (α := ℕ∞) 1 (y * z) = HPow.hPow (α := ℕ∞) 1 y ^ z
inr₂ : ∀ (x_2 : 1 < x), x ^ (y * z) = (x ^ y) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rcases lt_trichotomy x 1 with x_0 | rfl | x_2

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
inr : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 y ^ z
inr₁ : HPow.hPow (α := ℕ∞) 0 (y * z) = HPow.hPow (α := ℕ∞) 0 z
inr₂ : HPow.hPow (α := ℕ∞) 0 (y * z) = 0
inr₃ inr₄ : Eq (α := ℕ∞) 0 0
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]

Premises used: ENat.zero_epow, Iff.mp, mul_ne_zero, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
⊢ HPow.hPow (α := ℕ∞) 1 (y * z) = HPow.hPow (α := ℕ∞) 1 y ^ z

Tactic:
simp only [one_epow]

Premises used: ENat.one_epow
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
inr : ∀ (y_0 : Ne (α := ℕ∞) ⊤ 0), x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z
inr₁ : ∀ (a : ℕ) (y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0), x ^ ((↑a : ℕ∞) * z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ^ z
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
induction y
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : Ne (α := ℕ∞) ⊤ 0
inr : HPow.hPow (β := ℕ∞) x ⊤ = HPow.hPow (β := ℕ∞) x ⊤ ^ z
inr₁ : ⊤ = HPow.hPow (α := ℕ∞) ⊤ z
inr₂ inr₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ x ^ (⊤ * z) = HPow.hPow (β := ℕ∞) x ⊤ ^ z

Tactic:
rw [top_mul z_0, epow_top x_2, top_epow z_0]

Premises used: ENat.top_epow, ENat.top_mul, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
inr :
  ∀ (z_0 : Ne (α := ℕ∞) ⊤ 0),
    x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
inr₁ :
  ∀ (a_1 : ℕ) (z_0 : Ne (α := ℕ∞) (↑a_1 : ℕ∞) 0),
    x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) (↑a_1 : ℕ∞)
⊢ x ^ ((↑a : ℕ∞) * z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ^ z

Tactic:
induction z
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
inr : ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤
⊢ x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤

Tactic:
rw [mul_top y_0, epow_top x_2]

Premises used: ENat.mul_top, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
apply : 1 < HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)
⊢ ⊤ = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) ⊤

Tactic:
apply (epow_top _).symm

Premises used: Eq.symm, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
apply : LT.lt (α := ℕ∞) 1 ((fun (y : ℕ∞) ↦ x ^ y) 1)
⊢ 1 < HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)

Tactic:
apply (epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)).trans_lt'

Premises used: Iff.mpr, ENat.epow_right_mono, LT.lt.le, LE.le.trans_lt', Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
z_0 : Ne (α := ℕ∞) ⊤ 0
⊢ LT.lt (α := ℕ∞) 1 ((fun (y : ℕ∞) ↦ x ^ y) 1)

Tactic:
simp only [x_2, epow_one]

Premises used: ENat.epow_one
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
y_0 : Ne (α := ℕ∞) (↑a : ℕ∞) 0
a_1 : ℕ
z_0 : Ne (α := ℕ∞) (↑a_1 : ℕ∞) 0
⊢ x ^ HMul.hMul (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) (HPow.hPow (β := ℕ∞) x (↑a : ℕ∞)) (↑a_1 : ℕ∞)

Tactic:
simp only [← Nat.cast_mul, epow_natCast, pow_mul x]

Premises used: ENat.epow_natCast, pow_mul, Nat.cast_mul
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ StrictMono Real.toEReal

Tactic:
WithBot.coe_strictMono.comp WithTop.coe_strictMono

Premises used: EReal, WithTop.coe_strictMono, StrictMono.comp, Real.toEReal, WithBot.coe_strictMono
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ Injective Real.toEReal

Tactic:
coe_strictMono.injective

Premises used: StrictMono.injective, EReal.coe_strictMono
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑x : EReal) ≤ (↑y : EReal) ↔ x ≤ y

Tactic:
coe_strictMono.le_iff_le

Premises used: EReal.coe_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑x : EReal) < (↑y : EReal) ↔ x < y

Tactic:
coe_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, EReal.coe_strictMono
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑x : EReal) = (↑y : EReal) ↔ x = y

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, EReal.coe_injective
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑x : EReal) ≠ (↑y : EReal) ↔ x ≠ y

Tactic:
coe_injective.ne_iff

Premises used: Function.Injective.ne_iff, EReal.coe_injective
-- Module: Mathlib.Data.EReal.Basic
Goal:
n : ℕ
⊢ (↑(↑n : ℝ) : EReal) = (↑n : EReal)

Tactic:
rfl

Premises used: WithBot.some, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ LE.le (α := EReal) (({ toFun := Real.toEReal, inj' := coe_injective : ℝ ↪ EReal } : (a : ℝ) → EReal) x : EReal)
      (({ toFun := Real.toEReal, inj' := coe_injective : ℝ ↪ EReal } : (a : ℝ) → EReal) y : EReal) ↔
    x ≤ y

Tactic:
simp
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (⇑orderEmbedding : (a : ℝ) → EReal) = Real.toEReal

Tactic:
rfl

Premises used: WithBot.some, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑0 : EReal) = 0

Tactic:
rfl

Premises used: WithBot.some, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
⊢ (↑1 : EReal) = 1

Tactic:
rfl

Premises used: WithBot.some, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
motive : EReal → Sort u_1
bot : motive ⊥
coe : (a : ℝ) → motive (↑a : EReal)
top : motive ⊤
⊢ EReal.rec (motive := fun (x : EReal) ↦ motive x) bot coe top ⊥ = bot

Tactic:
rfl

Premises used: EReal.rec, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
motive : EReal → Sort u_1
bot : motive ⊥
coe : (a : ℝ) → motive (↑a : EReal)
top : motive ⊤
⊢ EReal.rec (motive := fun (x : EReal) ↦ motive x) bot coe top ⊤ = top

Tactic:
rfl

Premises used: EReal.rec, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
motive : EReal → Sort u_1
bot : motive ⊥
coe : (a : ℝ) → motive (↑a : EReal)
top : motive ⊤
a : ℝ
⊢ EReal.rec (motive := fun (x : EReal) ↦ motive x) bot coe top (↑a : EReal) = coe a

Tactic:
rfl

Premises used: EReal.rec, rfl
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
r : EReal
hr : p r
bot : ∀ (hr : p ⊥), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
coe : ∀ (a : ℝ) (hr : p (↑a : EReal)), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
top : ∀ (hr : p ⊤), p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)

Tactic:
cases r
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
hr : p ⊥
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
a : ℝ
hr : p (↑a : EReal)
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
hr : p ⊤
⊢ p ⊥ ∨ p ⊤ ∨ ∃ (r : ℝ), p (↑r : EReal)

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
h : p ⊥
⊢ ∃ (r : EReal), p r

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
h : p ⊥
⊢ ∃ (r : EReal), p r

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
h : p ⊤
⊢ ∃ (r : EReal), p r

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
h : p ⊤
⊢ ∃ (r : EReal), p r

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
r : ℝ
hr : p (↑r : EReal)
⊢ ∃ (r : EReal), p r

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.EReal.Basic
Goal:
p : EReal → Prop
r : ℝ
hr : p (↑r : EReal)
⊢ ∃ (r : EReal), p r

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Data.EReal.Basic
Goal:
x y : ℝ
⊢ (↑(x * y) : EReal) = (↑x : EReal) * (↑y : EReal)

Tactic:
rfl

Premises used: WithBot.some, EReal.mul, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊥ (↑y : EReal)
inr : P ⊥ (↑0 : EReal)
inr₁ : ∀ (hy : 0 < y), P ⊥ (↑y : EReal)
⊢ P ⊥ (↑y : EReal)

Tactic:
rcases lt_trichotomy y 0 with (hy | rfl | hy)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊥ (↑y : EReal)

Tactic:
bot_neg y hy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
⊢ P ⊥ (↑0 : EReal)

Tactic:
bot_zero

Premises used: WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
hy : 0 < y
⊢ P ⊥ (↑y : EReal)

Tactic:
bot_pos y hy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊥ (↑y : EReal)

Tactic:
exacts [bot_neg y hy, bot_zero, bot_pos y hy]
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊥
inr : P (↑0 : EReal) ⊥
inr₁ : ∀ (hx : 0 < x), P (↑x : EReal) ⊥
⊢ P (↑x : EReal) ⊥

Tactic:
rcases lt_trichotomy x 0 with (hx | rfl | hx)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P (↑x : EReal) ⊥

Tactic:
neg_bot x hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
⊢ P (↑0 : EReal) ⊥

Tactic:
zero_bot

Premises used: WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : 0 < x
⊢ P (↑x : EReal) ⊥

Tactic:
pos_bot x hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P (↑x : EReal) ⊥

Tactic:
exacts [neg_bot x hx, zero_bot, pos_bot x hx]
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
inl : ∀ (hx : x < 0), P (↑x : EReal) ⊤
inr : P (↑0 : EReal) ⊤
inr₁ : ∀ (hx : 0 < x), P (↑x : EReal) ⊤
⊢ P (↑x : EReal) ⊤

Tactic:
rcases lt_trichotomy x 0 with (hx | rfl | hx)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P (↑x : EReal) ⊤

Tactic:
neg_top x hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
⊢ P (↑0 : EReal) ⊤

Tactic:
zero_top

Premises used: WithBot.some, Real.toEReal
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : 0 < x
⊢ P (↑x : EReal) ⊤

Tactic:
pos_top x hx
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
x : ℝ
hx : x < 0
⊢ P (↑x : EReal) ⊤

Tactic:
exacts [neg_top x hx, zero_top, pos_top x hx]
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
inl : ∀ (hy : y < 0), P ⊤ (↑y : EReal)
inr : P ⊤ (↑0 : EReal)
inr₁ : ∀ (hy : 0 < y), P ⊤ (↑y : EReal)
⊢ P ⊤ (↑y : EReal)

Tactic:
rcases lt_trichotomy y 0 with (hy | rfl | hy)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.EReal.Basic
Goal:
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P (↑x : EReal) ⊤
neg_bot : ∀ x < 0, P (↑x : EReal) ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ (↑x : EReal)
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ (↑x : EReal)
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊤ (↑y : EReal)

Tactic:
top_neg y hy