awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.Lattice
Goal:
a : ℕ∞
s : Set ℕ∞
rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
rw₁ rw₂ : Eq (α := ℕ∞) (⨅ i ∈ s, a + i) (⨅ b ∈ s, a + b)
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
rw [sInf_eq_iInf, add_iInf₂]

Premises used: sInf_eq_iInf, ENat.add_iInf₂
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
simp_rw : a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b
⊢ a ≤ iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Premises used: ENat.add_iInf, ENat.iInf_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b

Tactic:
le_iInf₂ h

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b

Tactic:
exact le_iInf₂ h

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
simp_rw : a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1
⊢ a ≤ HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) (⨅ (k : κ), ⨅ (qk : q₂ k), g k qk)

Tactic:
simp_rw [iInf₂_add, add_iInf₂]

Premises used: ENat.add_iInf₂, ENat.iInf₂_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1

Tactic:
le_iInf₂ fun i hi => le_iInf₂ (h i hi)

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
κ : Sort u_4
q₁ : ι → Sort u_5
q₂ : κ → Sort u_6
f : (i : ι) → q₁ i → ℕ∞
g : (k : κ) → q₂ k → ℕ∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1

Tactic:
exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
top : HPow.hPow (β := ℕ∞) x ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ = if LT.lt (α := ℕ∞) ⊤ ⊤ then x ^ toNat ⊤ else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
simp only [lt_self_iff_false, ↓reduceIte]

Premises used: lt_self_iff_false, reduceIte
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
⊢ HPow.hPow (β := ℕ∞) x ⊤ = if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
n : ℕ
coe : HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) = x ^ n
⊢ HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) =
    if LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤ then x ^ toNat (↑n : ℕ∞) else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
simp only [coe_lt_top, ↓reduceIte, toNat_coe]

Premises used: reduceIte, ENat.toNat_coe, ENat.coe_lt_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
n : ℕ
⊢ HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) = x ^ n

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
top : HPow.hPow (β := ℕ∞) x ⊤ = if LT.lt (α := ℕ∞) ⊤ ⊤ then x ^ toNat ⊤ else if x = 0 then 0 else if x = 1 then 1 else ⊤
coe :
  ∀ (n : ℕ),
    HPow.hPow (β := ℕ∞) x (↑n : ℕ∞) =
      if LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤ then x ^ toNat (↑n : ℕ∞) else if x = 0 then 0 else if x = 1 then 1 else ⊤
⊢ x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
cases y with
  | top => simp only [lt_self_iff_false, ↓reduceIte]; rfl
  | coe n => simp only [coe_lt_top, ↓reduceIte, toNat_coe]; rfl

Premises used: lt_self_iff_false, reduceIte, ENat.toNat_coe, ENat.coe_lt_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
y : ℕ
⊢ HPow.hPow (β := ℕ∞) x (↑y : ℕ∞) = x ^ y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0

Tactic:
rfl

Premises used: WithTop.some, rfl, ite
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : Ne (α := ℕ∞) ⊤ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0

Tactic:
zero_epow_top

Premises used: ENat.zero_epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : Ne (α := ℕ∞) ⊤ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0

Tactic:
exact zero_epow_top

Premises used: ENat.zero_epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) 0 y = 0
coe₁ : Eq (α := ℕ∞) 0 0 ∧ y ≠ 0
coe₂ : True ∧ y ≠ 0
coe₃ : y ≠ 0
coe₄ coe₅ coe₆ coe₇ : Ne (α := ℕ∞) (↑y : ℕ∞) 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0

Tactic:
rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Premises used: ENat.epow_natCast, pow_eq_zero_iff', eq_self, OfNat.ofNat, true_and, Nat.cast_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : y ≠ 0
top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 ⊤ = 0
coe : ∀ (y : ℕ) (h : Ne (α := ℕ∞) (↑y : ℕ∞) 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 (↑y : ℕ∞) = 0
⊢ HPow.hPow (α := ℕ∞) 0 y = 0

Tactic:
induction y with
  | top => exact zero_epow_top
  | coe y => rwa [epow_natCast, pow_eq_zero_iff', eq_self 0, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Premises used: ENat.epow_natCast, pow_eq_zero_iff', eq_self, OfNat.ofNat, ENat.zero_epow_top, true_and
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ = 1

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
y_1 : ℕ∞
y : ℕ
coe : HPow.hPow (α := ℕ∞) 1 y = 1
coe₁ coe₂ : Eq (α := ℕ∞) 1 1
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 (↑y : ℕ∞) = 1

Tactic:
rw [epow_natCast, one_pow]

Premises used: one_pow, ENat.epow_natCast
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
top : HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ = 1
coe : ∀ (y : ℕ), HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 (↑y : ℕ∞) = 1
⊢ HPow.hPow (α := ℕ∞) 1 y = 1

Tactic:
induction y with
  | top => rfl
  | coe y => rw [epow_natCast, one_pow]

Premises used: one_pow, ENat.epow_natCast
-- Module: Mathlib.Data.ENat.Pow
Goal:
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : Ne (α := ℕ∞) ⊤ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤

Tactic:
top_epow_top

Premises used: ENat.top_epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : Ne (α := ℕ∞) ⊤ 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤

Tactic:
exact top_epow_top

Premises used: ENat.top_epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y_1 : ℕ∞
y : ℕ
h : Ne (α := ℕ∞) (↑y : ℕ∞) 0
coe : HPow.hPow (α := ℕ∞) ⊤ y = ⊤
coe₁ : Eq (α := ℕ∞) ⊤ ⊤ ∧ y ≠ 0
coe₂ : True ∧ y ≠ 0
coe₃ : y ≠ 0
coe₄ coe₅ coe₆ coe₇ : Ne (α := ℕ∞) (↑y : ℕ∞) 0
⊢ HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤

Tactic:
rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Premises used: ENat.epow_natCast, ENat.pow_eq_top_iff, eq_self, Top.top, true_and, Nat.cast_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
h : y ≠ 0
top : ∀ (h : Ne (α := ℕ∞) ⊤ 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ ⊤ = ⊤
coe : ∀ (y : ℕ) (h : Ne (α := ℕ∞) (↑y : ℕ∞) 0), HPow.hPow (α := ℕ∞) (β := ℕ∞) ⊤ (↑y : ℕ∞) = ⊤
⊢ HPow.hPow (α := ℕ∞) ⊤ y = ⊤

Tactic:
induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Premises used: ENat.epow_natCast, ENat.top_epow_top, ENat.pow_eq_top_iff, eq_self, Top.top, true_and
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑0 : ℕ∞) = 1
rw₁ : HPow.hPow (β := ℕ) x 0 = 1
rw₂ rw₃ : Eq (α := ℕ∞) 1 1
⊢ HPow.hPow (β := ℕ∞) x 0 = 1

Tactic:
rw [← coe_zero, epow_natCast, pow_zero]

Premises used: ENat.epow_natCast, pow_zero, ENat.coe_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
rw : HPow.hPow (β := ℕ∞) x (↑1 : ℕ∞) = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
rw₂ rw₃ : x = x
⊢ HPow.hPow (β := ℕ∞) x 1 = x

Tactic:
rw [← coe_one, epow_natCast, pow_one]

Premises used: ENat.coe_one, ENat.epow_natCast, pow_one
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : 1 < x
⊢ LE.le (α := ℕ∞) 0 1

Tactic:
have : (0 : ℕ∞) ≤ 1 := zero_le_one
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
hnc : ¬x = 1
hnc₁ : ¬x = 0
hnc₂ : ¬LT.lt (α := ℕ∞) ⊤ ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ = ⊤

Tactic:
rw [epow_def, if_neg, if_neg, if_neg]

Premises used: ENat.epow_def, if_neg
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
⊢ ¬x = 1

Tactic:
grind
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
⊢ ¬x = 0

Tactic:
grind
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : 1 < x
this : LE.le (α := ℕ∞) 0 1
⊢ ¬LT.lt (α := ℕ∞) ⊤ ⊤

Tactic:
grind
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
y z : ℕ∞
y_z : y ≤ z
top : ∀ (y_z : ⊤ ≤ z), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) z)
coe : ∀ (a : ℕ) (y_z : (↑a : ℕ∞) ≤ z), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) z)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) y) ((fun (y : ℕ∞) ↦ x ^ y) z)

Tactic:
induction y
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
z : ℕ∞
y_z : ⊤ ≤ z
top top₁ : LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) ⊤) ((fun (y : ℕ∞) ↦ x ^ y) z)

Tactic:
rw [top_le_iff.1 y_z]

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
z : ℕ∞
a : ℕ
y_z : (↑a : ℕ∞) ≤ z
coe :
  ∀ (y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
coe₁ :
  ∀ (a_1 : ℕ) (y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)),
    LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) (↑a_1 : ℕ∞))
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) z)

Tactic:
induction z
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
coe : ∀ (x_0 : x < 1), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
coe₁ :
  ∀ (h : Ne (α := ℕ∞) 1 0),
    LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) ⊤)
coe₂ : ∀ (x_2 : 1 < x), LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ 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 : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
x_0 : x < 1
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)

Tactic:
(h (lt_one_iff_eq_zero.1 x_0)).rec

Premises used: LE.le, Nat.cast, HPow.hPow, Iff.mp, False.rec, Top.top, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
x_0 : x < 1
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)

Tactic:
exact (h (lt_one_iff_eq_zero.1 x_0)).rec
-- Module: Mathlib.Data.ENat.Pow
Goal:
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
h : Ne (α := ℕ∞) 1 0
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ HPow.hPow (α := ℕ∞) 1 y) ⊤)

Tactic:
simp only [one_epow, le_refl]

Premises used: le_refl, ENat.one_epow
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
a : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) ⊤
x_2 : 1 < x
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) ⊤)

Tactic:
simp only [epow_top x_2, le_top]

Premises used: le_top, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
a a_1 : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) (↑a_1 : ℕ∞))

Tactic:
pow_right_mono₀ (one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)

Premises used: Iff.mpr, pow_right_mono₀, Iff.mp, Nat.cast_le, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x : ℕ∞
h : x ≠ 0
a a_1 : ℕ
y_z : LE.le (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) (↑a : ℕ∞)) ((fun (y : ℕ∞) ↦ x ^ y) (↑a_1 : ℕ∞))

Tactic:
exact pow_right_mono₀ (one_le_iff_ne_zero.2 h) (Nat.cast_le.1 y_z)

Premises used: Iff.mpr, pow_right_mono₀, Iff.mp, Nat.cast_le, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y

Tactic:
simpa using epow_right_mono h zero_le

Premises used: zero_le, ENat.epow_right_mono
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
top : HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
coe : ∀ (a : ℕ), HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≤ HPow.hPow (β := ℕ∞) z (↑a : ℕ∞)
⊢ x ^ y ≤ z ^ y

Tactic:
induction y
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
top : ∀ (x_0 : x < 1), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
top₁ : ∀ (x_z : 1 ≤ z), HPow.hPow (α := ℕ∞) (β := ℕ∞) 1 ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
top₂ : ∀ (x_2 : 1 < x), HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) 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:
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
top : 0 ≤ HPow.hPow (β := ℕ∞) z ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
rw [lt_one_iff_eq_zero.1 x_0, zero_epow_top]

Premises used: Iff.mp, ENat.zero_epow_top, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
bot_le

Premises used: WithTop.some, bot_le
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_0 : x < 1
⊢ 0 ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Data.ENat.Pow
Goal:
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
one_le_epow (one_le_iff_ne_zero.1 x_z)

Premises used: ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y z : ℕ∞
x_z : 1 ≤ z
⊢ 1 ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
exact one_le_epow (one_le_iff_ne_zero.1 x_z)

Premises used: ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
top : HPow.hPow (β := ℕ∞) x ⊤ ≤ ⊤
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ HPow.hPow (β := ℕ∞) z ⊤

Tactic:
rw [epow_top (x_2.trans_le x_z)]

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

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ HPow.hPow (β := ℕ∞) x ⊤ ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
y x z : ℕ∞
x_z : x ≤ z
a : ℕ
⊢ HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≤ HPow.hPow (β := ℕ∞) z (↑a : ℕ∞)

Tactic:
simp only [epow_natCast, (pow_left_mono _) x_z]

Premises used: ENat.epow_natCast, pow_left_mono
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩

Premises used: ENat.zero_epow, Eq.rec, And.right, And.left, And.intro, Iff.intro, Eq.symm
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
refine_1 : ∀ (h : x ^ y = 0), x = 0
refine_2 : ∀ (h : x ^ y = 0) (y_0 : y = 0), False
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
refine ⟨fun h ↦ ⟨?_, fun y_0 ↦ ?_⟩, fun h ↦ h.1.symm ▸ zero_epow h.2⟩
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 0
refine_1 : ∀ (x_0 : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra x_0
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 0
x_0 : ¬x = 0
⊢ False

Tactic:
(one_le_iff_ne_zero.1 (one_le_epow (y := y) x_0) h).rec

Premises used: False, ENat.one_le_epow, Iff.mp, False.rec, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 0
x_0 : ¬x = 0
⊢ False

Tactic:
exact (one_le_iff_ne_zero.1 (one_le_epow (y := y) x_0) h).rec
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
⊢ Eq (α := ℕ∞) 1 0

Tactic:
rw [y_0, epow_zero] at h

Premises used: ENat.epow_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 0
y_0 : y = 0
h₁ : Eq (α := ℕ∞) 1 0
⊢ y = 0

Tactic:
rw [y_0, epow_zero] at h

Premises used: ENat.epow_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : Eq (α := ℕ∞) 1 0
y_0 : y = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x = 1 ∨ y = 0
inl : ∀ (h : x = 1), x ^ y = 1
inr : ∀ (h : y = 0), x ^ y = 1
⊢ x ^ y = 1

Tactic:
rcases h with h | h
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x = 1
⊢ x ^ y = 1

Tactic:
simp [h]
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : y = 0
⊢ x ^ y = 1

Tactic:
simp [h]
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
refine : ∀ (h : x ^ y = 1) (y_0 : ¬y = 0), x = 1
⊢ x ^ y = 1 ↔ x = 1 ∨ y = 0

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_right.2 fun y_0 ↦ ?_, fun h ↦ by rcases h with h | h <;> simp [h]⟩
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
inl : ∀ (x_0 : x < 1), x = 1
inr : ∀ (h : HPow.hPow (α := ℕ∞) 1 y = 1), Eq (α := ℕ∞) 1 1
inr₁ : ∀ (x_2 : 1 < x), x = 1
⊢ x = 1

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 : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ Eq (α := ℕ∞) 0 1

Tactic:
rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h

Premises used: ENat.zero_epow, Iff.mp, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
h₁ : Eq (α := ℕ∞) 0 1
⊢ ¬y = 0

Tactic:
rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h

Premises used: ENat.zero_epow, Iff.mp, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
h₁ : Eq (α := ℕ∞) 0 1
y_0₁ : ¬y = 0
⊢ x < 1

Tactic:
rw [lt_one_iff_eq_zero.1 x_0, zero_epow y_0] at h

Premises used: ENat.zero_epow, Iff.mp, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : Eq (α := ℕ∞) 0 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

Tactic:
contradiction
-- Module: Mathlib.Data.ENat.Pow
Goal:
y : ℕ∞
y_0 : ¬y = 0
h : HPow.hPow (α := ℕ∞) 1 y = 1
⊢ Eq (α := ℕ∞) 1 1

Tactic:
rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) 1) ((fun (y : ℕ∞) ↦ x ^ y) y)

Tactic:
have := epow_right_mono (one_le_iff_ne_zero.1 x_2.le) (one_le_iff_ne_zero.2 y_0)
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : LE.le (α := ℕ∞) ((fun (y : ℕ∞) ↦ x ^ y) 1) ((fun (y : ℕ∞) ↦ x ^ y) y)
⊢ x ≤ 1

Tactic:
simp only [epow_one, h] at this

Premises used: ENat.epow_one
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : x ≤ 1
⊢ x = 1

Tactic:
(not_lt_of_ge this x_2).rec

Premises used: False.rec, OfNat.ofNat, Eq, not_lt_of_ge
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : x ≤ 1
⊢ x = 1

Tactic:
exact (not_lt_of_ge this x_2).rec
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
inl : ∀ (x_0 : x < 1), x ^ (y + z) = x ^ y * x ^ z
inr : HPow.hPow (α := ℕ∞) 1 (y + z) = HPow.hPow (α := ℕ∞) 1 y * HPow.hPow (α := ℕ∞) 1 z
inr₁ : ∀ (x_2 : 1 < x), x ^ (y + z) = x ^ y * x ^ z
⊢ x ^ (y + z) = x ^ y * x ^ 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 : ℕ∞
x_0 : x < 1
inl : HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rw [lt_one_iff_eq_zero.1 x_0]

Premises used: Iff.mp, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_0 : x < 1
inl : HPow.hPow (α := ℕ∞) 0 (0 + z) = HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 0 * HPow.hPow (α := ℕ∞) 0 z
inl₁ : ∀ (y_0 : 0 < y), HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z

Tactic:
rcases eq_zero_or_pos y with rfl | y_0

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Data.ENat.Pow
Goal:
x z : ℕ∞
x_0 : x < 1
⊢ HPow.hPow (α := ℕ∞) 0 (0 + z) = HPow.hPow (α := ℕ∞) (β := ℕ∞) 0 0 * HPow.hPow (α := ℕ∞) 0 z

Tactic:
simp only [zero_add, epow_zero, one_mul]

Premises used: zero_add, one_mul, ENat.epow_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
inl : HPow.hPow (α := ℕ∞) 0 (y + z) = 0
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = HPow.hPow (α := ℕ∞) 0 y * HPow.hPow (α := ℕ∞) 0 z

Tactic:
rw [zero_epow y_0.ne.symm, zero_mul]

Premises used: MulZeroClass.zero_mul, ENat.zero_epow, Ne.symm, LT.lt.ne
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = 0

Tactic:
zero_epow (add_pos_of_pos_of_nonneg y_0 bot_le).ne.symm

Premises used: ENat.zero_epow, Ne.symm, bot_le, add_pos_of_pos_of_nonneg, LT.lt.ne
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_0 : x < 1
y_0 : 0 < y
⊢ HPow.hPow (α := ℕ∞) 0 (y + z) = 0

Tactic:
exact zero_epow (add_pos_of_pos_of_nonneg y_0 bot_le).ne.symm

Premises used: ENat.zero_epow, Ne.symm, bot_le, add_pos_of_pos_of_nonneg, LT.lt.ne
-- Module: Mathlib.Data.ENat.Pow
Goal:
y z : ℕ∞
⊢ HPow.hPow (α := ℕ∞) 1 (y + z) = HPow.hPow (α := ℕ∞) 1 y * HPow.hPow (α := ℕ∞) 1 z

Tactic:
simp only [one_epow, mul_one]

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

Tactic:
induction y
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
inr : x ^ z ≠ 0
⊢ x ^ (⊤ + z) = HPow.hPow (β := ℕ∞) x ⊤ * x ^ z

Tactic:
rw [top_add, epow_top x_2, top_mul]

Premises used: top_add, ENat.top_mul, ENat.epow_top
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ z ≠ 0

Tactic:
one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))

Premises used: LT.lt.le, ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ z ≠ 0

Tactic:
exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))

Premises used: LT.lt.le, ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
inr : x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x ⊤
inr₁ :
  ∀ (a_1 : ℕ),
    x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x (↑a_1 : ℕ∞)
⊢ x ^ ((↑a : ℕ∞) + z) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * x ^ z

Tactic:
induction z
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
inr : HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≠ 0
⊢ x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤ = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x ⊤

Tactic:
rw [add_top, epow_top x_2, mul_top]

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

Tactic:
one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))

Premises used: LT.lt.le, ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a : ℕ
⊢ HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) ≠ 0

Tactic:
exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))

Premises used: LT.lt.le, ENat.one_le_epow, Iff.mp, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
x_2 : 1 < x
a a_1 : ℕ
⊢ x ^ HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) x (↑a_1 : ℕ∞)

Tactic:
simp only [← Nat.cast_add, epow_natCast, pow_add x]

Premises used: ENat.epow_natCast, pow_add, Nat.cast_add
-- Module: Mathlib.Data.ENat.Pow
Goal:
x y z : ℕ∞
top : HPow.hPow (β := ℕ∞) (x * y) ⊤ = HPow.hPow (β := ℕ∞) x ⊤ * HPow.hPow (β := ℕ∞) y ⊤
coe :
  ∀ (a : ℕ), HPow.hPow (β := ℕ∞) (x * y) (↑a : ℕ∞) = HPow.hPow (β := ℕ∞) x (↑a : ℕ∞) * HPow.hPow (β := ℕ∞) y (↑a : ℕ∞)
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
induction z