awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
this : Invertible (α := α) (↑n.succ : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ
have generalize : ∀ (n : ℕ) (this : Invertible (α := α) (↑n : α)),
  IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n
Tactic: generalize Nat.succ n = n at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Inv (goal)
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n_1 d : ℕ
inv : Invertible (α := α) (↑d : α)
n : ℕ
this : Invertible (α := α) (↑n : α)
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n
have eq : (HMul.hMul (α := α) (↑(-Int.ofNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ =
  HMul.hMul (α := α) (↑(-Int.ofNat d) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n : α) _)
Tactic: use this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
⊢ Irrational (Real.rpow (↑q : ℝ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : ℝ))
have simp : ∀ (x : ℚ), ¬(↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
Tactic: simp only [Irrational, Rat.cast_div, Rat.cast_natCast, Real.rpow_eq_pow, Set.mem_range,
    not_exists]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : (↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ False
have absurd : q ^ a = x ^ b
Tactic: absurd h x
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : (↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ q ^ a = x ^ b
have rify : HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (↑x : ℝ) b
Tactic: rify
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : (↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ Ne (α := ℝ) (↑b : ℝ) 0
have simp : ¬b = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
hx : (↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (↑x : ℝ) b
have rw : HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (β := ℝ) (↑q : ℝ) (↑a : ℝ)
Tactic: rw [hx, ← Real.rpow_mul_natCast (by simpa), div_mul_cancel₀ _ (by simp; lia)]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q
have inl : ∀ (h : ∀ (m : ℕ), 0 ≠ m ^ q), HPow.hPow (α := ℕ) 0 p ≠ m ^ q
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
inl : ∀ (h : ∀ (m : ℕ), 0 ≠ m ^ q), HPow.hPow (α := ℕ) 0 p ≠ m ^ q
⊢ n ^ p ≠ m ^ q
have inr : ∀ (hn : n ≠ 0), n ^ p ≠ m ^ q
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
hn : n ≠ 0
⊢ n ^ p ≠ m ^ q
have inr : ∀ (h : n ^ p = m ^ q), ∃ (m : ℕ), n = m ^ q
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
⊢ ∃ (m : ℕ), n = m ^ q
have hf0 : Eq (α := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: have hf0 : f 0 = 0 := by simpa [hq.ne'] using congr($hf 0)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : Eq (α := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ ∃ (m : ℕ), n = m ^ q
have refine : n.factorization = (HPow.hPow (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) q).factorization
Tactic: refine ⟨f.prod (· ^ ·), Nat.factorization_inj hn (by simp [hf0]) ?_⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
hf : n.factorization = q • f
hf0 : Eq (α := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ n.factorization = (HPow.hPow (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) q).factorization
have rwa : f ≤ n.factorization
Tactic: rwa [Nat.factorization_pow, n.factorization_prod_pow_eq_self_of_le_factorization ?_]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
⊢ ∃ (m : ℕ), n = m ^ q
have inr : n.factorization = q • f
Tactic: suffices hf : n.factorization = q • f by
    have hf0 : f 0 = 0 := by simpa [hq.ne'] using congr($hf 0)
    refine ⟨f.prod (· ^ ·), Nat.factorization_inj hn (by simp [hf0]) ?_⟩
    rwa [Nat.factorization_pow, n.factorization_prod_pow_eq_self_of_le_factorization ?_]
    exact hf ▸ le_self_nsmul zero_le (by lia)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
⊢ n.factorization = q • f
have inr : ∀ (z : ℕ), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) z : ℕ) ((q • f : (a : ℕ) → ℕ) z : ℕ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun (x : ℕ) ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) z : ℕ) ((q • f : (a : ℕ) → ℕ) z : ℕ)
have inr : q ∣ (n.factorization : (a : ℕ) → ℕ) z
Tactic: rw [Finsupp.smul_apply, smul_eq_mul, Finsupp.mapRange_apply, Nat.mul_div_cancel']
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
h : n = m ^ d
⊢ False
have h_right₁ : m ^ d < (k + 1) ^ d
Tactic: rw [h] at h_left h_right
Cleared hypotheses: h_left, h_right, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
h : n = m ^ d
h_right₁ : m ^ d < (k + 1) ^ d
⊢ False
have h_left₁ : k ^ d < m ^ d
Tactic: rw [h] at h_left h_right
Cleared hypotheses: h_left, h_right, h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
⊢ False
have this : k < m
Tactic: have : k < m := lt_of_pow_lt_pow_left' d h_left
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this : k < m
⊢ False
have this₁ : m < k + 1
Tactic: have : m < k + 1 := lt_of_pow_lt_pow_left' d h_right
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ n ^ p ≠ m ^ q
have h : ∀ (m : ℕ), n ≠ m ^ q
Tactic: apply not_power_nat_pow h_coprime hq
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a = y
have a₁ : a ∣ y
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
a₁ : a ∣ y
⊢ a = y
have a₂ : y ∣ a
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y * b = x * a
have rw : b * y = x * a
Tactic: rw [mul_comm, ← h, mul_comm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
rw : b * y = x * a
⊢ y * b = x * a
have rw₁ : a * x = x * a
Tactic: rw [mul_comm, ← h, mul_comm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
rw : b * y = x * a
rw₁ : a * x = x * a
⊢ y * b = x * a
have rw₂ : x * a = x * a
Tactic: rw [mul_comm, ← h, mul_comm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have pos : ∀ (hb_zero : b = 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: by_cases hb_zero : b = 0
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
pos : ∀ (hb_zero : b = 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg : ∀ (hb_zero : ¬b = 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: by_cases hb_zero : b = 0
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : b = 0
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have pos : ∀ (h_coprime : a.Coprime 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) ≠ q ^ d
Tactic: subst hb_zero
Cleared hypotheses: b, h_coprime, hb_zero
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a d : ℕ
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
h_coprime : a.Coprime 0
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) ≠ q ^ d
have pos : ∀ (ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d), ∃ (x : ℕ), a = x ^ d
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a d : ℕ
q : ℚ
hq : 0 ≤ q
h_coprime : a.Coprime 0
ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d
⊢ ∃ (x : ℕ), a = x ^ d
have h_coprime₁ : a = 1
Tactic: simp only [Nat.coprime_zero_right] at h_coprime
Cleared hypotheses: h_coprime
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a d : ℕ
q : ℚ
hq : 0 ≤ q
ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d
h_coprime : a = 1
⊢ ∃ (x : ℕ), a = x ^ d
have pos : ∀ (ha : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑0 : ℚ) = q ^ d), ∃ (x : ℕ), 1 = x ^ d
Tactic: subst h_coprime
Cleared hypotheses: a, ha, h_coprime
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑0 : ℚ) = q ^ d
⊢ ∃ (x : ℕ), 1 = x ^ d
have h : 1 = HPow.hPow (α := ℕ) 1 d
Tactic: use 1
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d
⊢ False
have h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) ^ d
Tactic: rw [← Rat.num_div_den q] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑x' : ℚ) (↑y : ℚ) ^ d
⊢ False
have neg : ∀ (x : ℕ) (hx' : x' = (↑x : ℤ)), False
Tactic: obtain ⟨x, hx'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ x' by rwa [Rat.num_nonneg])
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑x' : ℚ) (↑y : ℚ) ^ d
x : ℕ
hx' : x' = (↑x : ℤ)
⊢ False
have h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
Tactic: rw [hx'] at h
Cleared hypotheses: h, hx'
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
hx' : x' = (↑x : ℤ)
⊢ False
have ha₁ : a ≠ x ^ d
Tactic: specialize ha x
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
⊢ False
have h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
Tactic: simp only [Int.cast_natCast, div_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
⊢ False
have neg : ∀ (h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)), False
Tactic: rw [div_eq_div_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
neg : ∀ (h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)), False
⊢ False
have neg₁ : Ne (α := ℚ) (↑b : ℚ) 0
Tactic: rw [div_eq_div_iff] at h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HPow.hPow (α := ℚ) (↑x : ℚ) d / HPow.hPow (α := ℚ) (↑y : ℚ) d
neg : ∀ (h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)), False
neg₁ : Ne (α := ℚ) (↑b : ℚ) 0
⊢ False
have neg₂ : HPow.hPow (α := ℚ) (↑y : ℚ) d ≠ 0
Tactic: rw [div_eq_div_iff] at h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : (↑a : ℚ) * HPow.hPow (α := ℚ) (↑y : ℚ) d = HPow.hPow (α := ℚ) (↑x : ℚ) d * (↑b : ℚ)
⊢ False
have h₁ : a * y ^ d = x ^ d * b
Tactic: replace h : a * y ^ d = x ^ d * b := by
    qify
    assumption
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
⊢ False
have neg : a = x ^ d
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
| a * y ^ d = x ^ d * b
have rhs : x ^ d * b
Tactic: rhs
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
| x ^ d * b
have rw : b * x ^ d
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
| a * y ^ d = x ^ d * b
have rw : b * x ^ d
Tactic: rhs; rw [mul_comm]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = x ^ d * b
⊢ a = x ^ d
have h₁ : a * y ^ d = b * x ^ d
Tactic: conv at h => rhs; rw [mul_comm]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
⊢ a = x ^ d
have apply : (y ^ d).Coprime (x ^ d)
Tactic: apply eq_of_mul_eq_mul_of_coprime h_coprime _ h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
⊢ (y ^ d).Coprime (x ^ d)
have H1 : y.Coprime (x ^ d)
Tactic: apply Nat.Coprime.pow_left
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
⊢ y.Coprime (x ^ d)
have H1 : y.Coprime x
Tactic: apply Nat.Coprime.pow_right
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
hx' : x' = (↑x : ℤ)
ha : a ≠ x ^ d
h : a * y ^ d = b * x ^ d
⊢ y.Coprime x
have H1 : x.Coprime y
Tactic: apply Nat.Coprime.symm
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have pos : ∀ (hq : 0 ≤ q), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: by_cases hq : 0 ≤ q
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
pos : ∀ (hq : 0 ≤ q), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg : ∀ (hq : ¬0 ≤ q), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: by_cases hq : 0 ≤ q
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg : ∀ (h_even : Even d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: rcases d.even_or_odd with (h_even | h_odd)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
neg : ∀ (h_even : Even d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg₁ : ∀ (h_odd : Odd d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: rcases d.even_or_odd with (h_even | h_odd)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
⊢ 0 ≤ -q
have linarith : -q < 0 → q - 0 + (-q - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have this : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ (-q) ^ d
Tactic: have := not_power_rat_of_num_aux h_coprime (q := -q) ha (by linarith)
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_even : Even d
this : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ (-q) ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg : ∀ (this : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
Tactic: rwa [h_even.neg_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : ¬0 ≤ q
h_odd : Odd d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
have neg : ∀ (hq : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d), 0 ≤ q
Tactic: contrapose hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
h_odd : Odd d
hq : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d
⊢ 0 ≤ q
have neg : 0 ≤ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)
Tactic: rw [← h_odd.pow_nonneg_iff, ← hq]
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
⊢ 0 < y_den
have by_contra! : ∀ (h : y_den ≤ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den ≤ 0
⊢ False
have h₁ : y_den = 0
Tactic: simp only [nonpos_iff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den = 0
⊢ False
have hn1₁ : 1 < x_num
Tactic: simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2
Cleared hypotheses: hn1, hn2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
h : y_den = 0
hn1₁ : 1 < x_num
⊢ False
have hn2₁ : x_num = 0
Tactic: simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2
Cleared hypotheses: hn1, hn2
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (hypothesis)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
⊢ Irrational (x ^ y)
have hy_den_pos : 0 < y_den
Tactic: have hy_den_pos : 0 < y_den := by
    by_contra! h
    simp only [nonpos_iff_eq_zero] at h
    simp only [h, pow_zero, Nat.lt_one_iff] at hn1 hn2
    lia
-- Lean 4 proof step from Mathlib.Tactic.NormNum.Irrational (goal)
Goal:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
⊢ Irrational (x ^ y)
have rcases : ∀ (hx_inv : Invertible (α := ℝ) (↑x_den : ℝ))
  (hx_eq :
    x = HMul.hMul (α := ℝ) (↑x_num : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑x_den : ℝ) _)),
  Irrational (x ^ y)
Tactic: rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩
Cleared hypotheses: hx_isNNRat