mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inr.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
<;>

Goal state after:
case pos.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.zero
⊢ ∞ ^ ↑0 = ∞ ^ 0

pp: case top.succ
n✝ : ℕ
⊢ ∞ ^ ↑(n✝ + 1) = ∞ ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case top.zero
⊢ ∞ ^ ↑0 = ∞ ^ 0

case top.succ
n✝ : ℕ
⊢ ∞ ^ ↑(n✝ + 1) = ∞ ^ (n✝ + 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case ofNat
x : ℝ≥0∞
a✝ : ℕ
⊢ x ^ ↑(Int.ofNat a✝) = x ^ Int.ofNat a✝

pp: case negSucc
x : ℝ≥0∞
a✝ : ℕ
⊢ x ^ ↑(Int.negSucc a✝) = x ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
x : ℝ≥0∞
a✝ : ℕ
⊢ x ^ ↑(Int.ofNat a✝) = x ^ Int.ofNat a✝

case negSucc
x : ℝ≥0∞
a✝ : ℕ
⊢ x ^ ↑(Int.negSucc a✝) = x ^ Int.negSucc a✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case e'_2
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ x * y = y * x

pp: case e'_3.h₁
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0

pp: case e'_3.h₃
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
a✝ : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0)
⊢ x ^ z * y ^ z = y ^ z * x ^ z

Tactic:
<;>

Goal state after:
case e'_2
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ x * y = y * x

case e'_3.h₁
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
⊢ (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 ↔ (y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0

case e'_3.h₃
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
this :
  ∀ (x y : ℝ≥0∞) (z : ℝ),
    z < 0 ∨ 0 < z → x ≤ y → (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
hxy : ¬x ≤ y
a✝ : ¬((y = 0 ∧ x = ∞ ∨ y = ∞ ∧ x = 0) ∧ z < 0)
⊢ x ^ z * y ^ z = y ^ z * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.top
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ ∞
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

pp: case inl.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

Tactic:
<;>

Goal state after:
case inl.top
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ ∞
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.top.inl
z : ℝ
hxy : 0 ≤ ∞
hz : z < 0
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

pp: case inl.top.inr
z : ℝ
hxy : 0 ≤ ∞
hz : 0 < z
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

pp: case inl.coe.inl
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : z < 0
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

pp: case inl.coe.inr
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : 0 < z
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

Tactic:
<;>

Goal state after:
case inl.top.inl
z : ℝ
hxy : 0 ≤ ∞
hz : z < 0
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.top.inr
z : ℝ
hxy : 0 ≤ ∞
hz : 0 < z
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.coe.inl
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : z < 0
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

case inl.coe.inr
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : 0 < z
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.top.inl
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : z < 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

pp: case inr.inr.top.inr
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : 0 < z
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

Tactic:
<;>

Goal state after:
case inr.inr.top.inl
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : z < 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

case inr.inr.top.inr
y : ℝ≥0∞
z : ℝ
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
hz : 0 < z
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ¬↑x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

Tactic:
coe_eq_zero

Goal state after:
case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe.top.inl
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : z < 0
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

pp: case inr.inr.coe.top.inr
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : 0 < z
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

Tactic:
<;>

Goal state after:
case inr.inr.coe.top.inl
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : z < 0
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

case inr.inr.coe.top.inr
z : ℝ
x✝ : ℝ≥0
hx0 : ¬x✝ = 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
hz : 0 < z
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

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

Goal state after:
case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inl.inl
y : ℝ
h✝ : y < 0
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

pp: case inr.inl.inr
y : ℝ
h✝ : 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

Tactic:
<;>

Goal state after:
case inr.inl.inl
y : ℝ
h✝ : y < 0
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

case inr.inl.inr
y : ℝ
h✝ : 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.inl.inl
y : ℝ
h0 : ∞ ≠ 0
h✝ : y < 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

pp: case inr.inr.inl.inr
y : ℝ
h0 : ∞ ≠ 0
h✝ : 0 < y
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

Tactic:
<;>

Goal state after:
case inr.inr.inl.inl
y : ℝ
h0 : ∞ ≠ 0
h✝ : y < 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

case inr.inr.inl.inr
y : ℝ
h0 : ∞ ≠ 0
h✝ : 0 < y
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
<;>

Goal state after:
case top.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
⊢ ∞ ^ y ≤ ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

pp: case top.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
<;>

Goal state after:
case top.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

case top.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ False

pp: case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ False

pp: case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ False

Tactic:
<;>

Goal state after:
case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ False

case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ False

case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
<;>

Goal state after:
case pos.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

pp: case pos.inr.inr.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
<;>

Goal state after:
case pos.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

case pos.inr.inr.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False

pp: case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False

pp: case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False

Tactic:
<;>

Goal state after:
case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False

case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False

case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ ↑n = a ^ n

Tactic:
Real.rpow_natCast

Goal state after:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ n = a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case h₁
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ a ≤ max a b

pp: case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ b ≤ max a b

Tactic:
<;>

Goal state after:
case h₁
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ a ≤ max a b

case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ b ≤ max a b
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case h₂.ha
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ a ^ p

pp: case hb
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ b ^ p

Tactic:
<;>

Goal state after:
case h₂.ha
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ a ^ p

case hb
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 0 ≤ b ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

pp: case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

pp: case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m

Tactic:
<;>

Goal state after:
case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑r

case hn
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ d ≠ 0

case hx
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ 0 ≤ ↑m
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z

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

Goal state after:
case inr.inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x z : M
hx : x ≠ 0
hz : z ≠ 0
hxy : SameRay R x 0
hyz : SameRay R 0 z
hy : 0 = 0 → x = 0 ∨ z = 0
⊢ SameRay R x z

case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
⊢ SameRay R x z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = ry • rx • x + rx • ry • y

pp: case e'_3
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z

Tactic:
<;>

Goal state after:
case e'_2
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = ry • rx • x + rx • ry • y

case e'_3
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (ry * rz₁ + rx * rz₂) • z = ry • rz₁ • z + rx • rz₂ • z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ rayOfNeZero R (u • v✝) ⋯ = rayOfNeZero R v✝ hv✝

Tactic:
ray_eq_iff

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ SameRay R (u • v✝) v✝
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = f 0 + f (x + y)

Tactic:
h0,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = 0 + f (x + y)
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) = f (midpoint R x y) + f (midpoint R x y)

Tactic:
by rw [← hm, midpoint_zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ ¬rayOfNeZero R x hx = rayOfNeZero R (-x) ⋯

Tactic:
ray_eq_iff

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)