awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num : ℤ
denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑denom : ℚ) * qi = 1
⊢ HMul.hMul (α := R) (↑denom : R) (↑qi : R) = 1

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num : ℤ
denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
simp : (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)
⊢ (↑(HMul.hMul (α := ℚ) (↑num : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : ℚ) _)) : R) =
    HMul.hMul (α := R) (↑num : R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : R) _)

Tactic:
simp only
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
num : ℤ
denom : ℕ
qi : ℚ
invOf_mul_self : qi * (↑denom : ℚ) = 1
mul_invOf_self : (↑denom : ℚ) * qi = 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑num : ℚ) * qi = (↑num : ℚ) * qi
⊢ (↑((↑num : ℚ) * qi) : R) = HMul.hMul (α := R) (↑num : R) (↑qi : R)

Tactic:
norm_cast
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionSemiring α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
have :
  ∀ (this : Invertible (α := α) (↑n.succ : α)),
    IsNNRat (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ d
      n.succ
⊢ IsNNRat (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ d
    n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionSemiring α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
this : Invertible (α := α) (↑n.succ : α)
⊢ (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ =
    HMul.hMul (α := α) (↑d : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n.succ : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionSemiring α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
this : Invertible (α := α) (↑n.succ : α)
⊢ IsNNRat (HMul.hMul (α := α) (↑n.succ : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ d
    n.succ

Tactic:
exact ⟨this, by simp⟩
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
have :
  ∀ (this : Invertible (α := α) (↑n.succ : α)),
    IsRat
      (HMul.hMul (α := α) (↑(Int.ofNat n.succ) : α)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
      (Int.ofNat d) n.succ
⊢ IsRat
    (HMul.hMul (α := α) (↑(Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
this : Invertible (α := α) (↑n.succ : α)
⊢ (HMul.hMul (α := α) (↑(Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹ =
    HMul.hMul (α := α) (↑(Int.ofNat d) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑n.succ : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
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

Tactic:
exact ⟨this, by simp⟩
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionSemiring α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α)⁻¹ (↑1 : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionSemiring α
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α)⁻¹ (↑0 : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negOfNat 1) : α)⁻¹ (↑(Int.negOfNat 1) : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
simp :
  IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ
⊢ IsRat
    (HMul.hMul (α := α) (↑(Int.negOfNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (Int.negOfNat d) n.succ

Tactic:
simp only [Int.negOfNat_eq]

Premises used: Int.negOfNat_eq
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
have :
  ∀ (this : Invertible (α := α) (↑n.succ : α)),
    IsRat
      (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
      (-Int.ofNat d) n.succ
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ

Tactic:
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
this : Invertible (α := α) (↑n.succ : α)
generalize :
  ∀ (n : ℕ) (this : Invertible (α := α) (↑n : α)),
    IsRat
      (HMul.hMul (α := α) (↑(-Int.ofNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
      (-Int.ofNat d) n
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n.succ) : α)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n.succ

Tactic:
generalize Nat.succ n = n at *

Premises used: Nat.succ
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n_1 d : ℕ
inv : Invertible (α := α) (↑d : α)
n : ℕ
this : Invertible (α := α) (↑n : α)
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 : α) _)
⊢ IsRat
    (HMul.hMul (α := α) (↑(-Int.ofNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _))⁻¹
    (-Int.ofNat d) n

Tactic:
use this
-- Module: Mathlib.Tactic.NormNum.Inv
Goal:
α : Type u_1
inst : DivisionRing α
inst_1 : CharZero α
n_1 d : ℕ
inv : Invertible (α := α) (↑d : α)
n : ℕ
this : Invertible (α := α) (↑n : α)
⊢ (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:
simp only [Int.ofNat_eq_natCast, Int.cast_neg,
    Int.cast_natCast, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]

Premises used: Int.cast_neg, Int.cast_natCast, inv_neg, Int.ofNat_eq_natCast, inv_inv, neg_mul, invOf_eq_inv, mul_inv_rev
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
simp : ∀ (x : ℚ), ¬(↑x : ℝ) = HPow.hPow (α := ℝ) (↑q : ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ Irrational (Real.rpow (↑q : ℝ) (↑(HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ)) : ℝ))

Tactic:
simp only [Irrational, Rat.cast_div, Rat.cast_natCast, Real.rpow_eq_pow, Set.mem_range,
    not_exists]

Premises used: Real.rpow_eq_pow, Set.mem_range, not_exists, Rat.cast_div, Irrational, Rat.cast_natCast
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
absurd : q ^ a = x ^ b
⊢ False

Tactic:
absurd h x
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
rify : HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (↑x : ℝ) b
⊢ q ^ a = x ^ b

Tactic:
rify
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
⊢ LE.le (α := ℝ) 0 (↑q : ℝ)

Tactic:
simpa
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
simp : ¬b = 0
⊢ Ne (α := ℝ) (↑b : ℝ) 0

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
⊢ ¬b = 0

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℝ))
rw : HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (β := ℝ) (↑q : ℝ) (↑a : ℝ)
⊢ HPow.hPow (α := ℝ) (↑q : ℝ) a = HPow.hPow (α := ℝ) (↑x : ℝ) b

Tactic:
rw [hx, ← Real.rpow_mul_natCast (by simpa), div_mul_cancel₀ _ (by simp; lia)]

Premises used: div_mul_cancel₀, Real.rpow_mul_natCast
-- Module: Mathlib.Tactic.NormNum.Irrational
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 (α := ℝ) (β := ℝ) (↑q : ℝ) (↑a : ℝ)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
inr : ∀ (hn : n ≠ 0), n ^ p ≠ m ^ q
⊢ n ^ p ≠ m ^ q

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
h : ∀ (m : ℕ), 0 ≠ m ^ q
⊢ HPow.hPow (α := ℕ) 0 p ≠ m ^ q

Tactic:
simpa [hq.ne'] using h 0

Premises used: LT.lt.ne', OfNat.ofNat
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
h : ∀ (m : ℕ), n ≠ m ^ q
m : ℕ
hn : n ≠ 0
inr : ∀ (h : n ^ p = m ^ q), ∃ (m : ℕ), n = m ^ q
⊢ n ^ p ≠ m ^ q

Tactic:
contrapose! h
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
⊢ Eq (α := ℕ) ((fun (x : ℕ) ↦ x / q) 0) 0

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ Eq (α := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
simpa [hq.ne'] using congr($hf 0)

Premises used: LT.lt.ne'
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ Eq (α := ℕ) ((f : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
have hf0 : f 0 = 0 := by simpa [hq.ne'] using congr($hf 0)
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ)
⊢ Membership.mem (γ := Set ℕ) {x : ℕ | x ≠ 0} (HPow.hPow (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) q)

Tactic:
simp [hf0]
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ)
refine : n.factorization = (HPow.hPow (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) q).factorization
⊢ ∃ (m : ℕ), n = m ^ q

Tactic:
refine ⟨f.prod (· ^ ·), Nat.factorization_inj hn (by simp [hf0]) ?_⟩
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ)
rwa : f ≤ n.factorization
⊢ n.factorization = (HPow.hPow (α := ℕ) (f.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) q).factorization

Tactic:
rwa [Nat.factorization_pow, n.factorization_prod_pow_eq_self_of_le_factorization ?_]

Premises used: Nat.factorization_prod_pow_eq_self_of_le_factorization, Nat.factorization_pow
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ)
⊢ q ≠ 0

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ)
⊢ f ≤ n.factorization

Tactic:
exact hf ▸ le_self_nsmul zero_le (by lia)
-- Module: Mathlib.Tactic.NormNum.Irrational
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
inr : n.factorization = q • f
⊢ ∃ (m : ℕ), n = m ^ q

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)
-- Module: Mathlib.Tactic.NormNum.Irrational
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
inr : ∀ (z : ℕ), Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) z : ℕ) ((q • f : (a : ℕ) → ℕ) z : ℕ)
⊢ n.factorization = q • f

Tactic:
ext z
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ
inr : q ∣ (n.factorization : (a : ℕ) → ℕ) z
⊢ Eq (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) z : ℕ) ((q • f : (a : ℕ) → ℕ) z : ℕ)

Tactic:
rw [Finsupp.smul_apply, smul_eq_mul, Finsupp.mapRange_apply, Nat.mul_div_cancel']

Premises used: Finsupp.mapRange_apply, Finsupp.smul_apply, smul_eq_mul, Nat.mul_div_cancel'
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ
⊢ HMul.hMul (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) z : ℕ) =
    HMul.hMul (β := ℕ) q ((m.factorization : (a : ℕ) → ℕ) z : ℕ)

Tactic:
simpa using congr(Nat.factorization $h z)
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ
⊢ q ∣ (n.factorization : (a : ℕ) → ℕ) z

Tactic:
simpa using h_coprime.symm.dvd_of_dvd_mul_left ⟨_, by simpa using congr(Nat.factorization $h z)⟩

Premises used: Nat.Coprime.symm, Exists.intro, Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
n k d : ℕ
h_left : k ^ d < n
h_right : n < (k + 1) ^ d
m : ℕ
h : n = m ^ d
⊢ m ^ d < (k + 1) ^ d

Tactic:
rw [h] at h_left h_right
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ k ^ d < m ^ d

Tactic:
rw [h] at h_left h_right
-- Module: Mathlib.Tactic.NormNum.Irrational
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
h_left₁ : k ^ d < m ^ d
⊢ n = m ^ d

Tactic:
rw [h] at h_left h_right
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
⊢ k < m

Tactic:
have : k < m := lt_of_pow_lt_pow_left' d h_left
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ m < k + 1

Tactic:
have : m < k + 1 := lt_of_pow_lt_pow_left' d h_right
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
n k d m : ℕ
h_right : m ^ d < (k + 1) ^ d
h_left : k ^ d < m ^ d
h : n = m ^ d
this_1 : k < m
this : m < k + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℕ
h : ∀ (m : ℕ), n ≠ m ^ q
⊢ n ^ p ≠ m ^ q

Tactic:
apply not_power_nat_pow h_coprime hq

Premises used: _private.0.Tactic.NormNum.not_power_nat_pow
-- Module: Mathlib.Tactic.NormNum.Irrational
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_1 m : ℕ
⊢ n ≠ m ^ q

Tactic:
apply not_power_nat_of_bounds h_left h_right

Premises used: _private.0.Tactic.NormNum.not_power_nat_of_bounds
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b x y : ℕ
hab : a.Coprime b
h : a * x = b * y
⊢ a ∣ y

Tactic:
Nat.Coprime.dvd_of_dvd_mul_left hab (Dvd.intro x h)

Premises used: Dvd.intro, Nat.Coprime.dvd_of_dvd_mul_left
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
a₁ : a ∣ y
a₂ : y ∣ a
⊢ a = y

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a ∣ y

Tactic:
eq_of_mul_eq_mul_of_coprime_aux hab h

Premises used: _private.0.Tactic.NormNum.eq_of_mul_eq_mul_of_coprime_aux
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ a ∣ y

Tactic:
exact eq_of_mul_eq_mul_of_coprime_aux hab h

Premises used: _private.0.Tactic.NormNum.eq_of_mul_eq_mul_of_coprime_aux
-- Module: Mathlib.Tactic.NormNum.Irrational
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
rw₂ rw₃ : x * a = x * a
⊢ y * b = x * a

Tactic:
rw [mul_comm, ← h, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b x y : ℕ
hab : a.Coprime b
hxy : x.Coprime y
h : a * x = b * y
⊢ y ∣ a

Tactic:
exact eq_of_mul_eq_mul_of_coprime_aux (x := b) hxy.symm (by rw [mul_comm, ← h, mul_comm])

Premises used: Nat.Coprime.symm, _private.0.Tactic.NormNum.eq_of_mul_eq_mul_of_coprime_aux
-- Module: Mathlib.Tactic.NormNum.Irrational
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
neg : ∀ (hb_zero : ¬b = 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
by_cases hb_zero : b = 0
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : b = 0
pos : ∀ (h_coprime : a.Coprime 0), HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) ≠ q ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
subst hb_zero
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a d : ℕ
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
h_coprime : a.Coprime 0
pos : ∀ (ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d), ∃ (x : ℕ), a = x ^ d
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) ≠ q ^ d

Tactic:
contrapose! ha
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a d : ℕ
q : ℚ
hq : 0 ≤ q
h_coprime : a.Coprime 0
ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d
⊢ a = 1

Tactic:
simp only [Nat.coprime_zero_right] at h_coprime

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a d : ℕ
q : ℚ
hq : 0 ≤ q
ha : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑0 : ℚ) = q ^ d
h_coprime : a = 1
pos : ∀ (ha : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑0 : ℚ) = q ^ d), ∃ (x : ℕ), 1 = x ^ d
⊢ ∃ (x : ℕ), a = x ^ d

Tactic:
subst h_coprime
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑0 : ℚ) = q ^ d
h : 1 = HPow.hPow (α := ℕ) 1 d
⊢ ∃ (x : ℕ), 1 = x ^ d

Tactic:
use 1
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
d : ℕ
q : ℚ
hq : 0 ≤ q
ha : HDiv.hDiv (α := ℚ) (↑1 : ℚ) (↑0 : ℚ) = q ^ d
⊢ 1 = HPow.hPow (α := ℕ) 1 d

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Irrational
Goal:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
neg : ∀ (h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = q ^ d), False
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) ≠ q ^ d

Tactic:
by_contra! h
-- Module: Mathlib.Tactic.NormNum.Irrational
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
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) ^ d

Tactic:
rw [← Rat.num_div_den q] at h

Premises used: Rat.num_div_den
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℚ) = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ) ^ d
⊢ let x' := q.num;
  HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑x' : ℚ) (↑q.den : ℚ) ^ d

Tactic:
set x' := q.num

Premises used: Rat.num
-- Module: Mathlib.Tactic.NormNum.Irrational
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
h : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑x' : ℚ) (↑q.den : ℚ) ^ d
⊢ let y := q.den;
  HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑x' : ℚ) (↑y : ℚ) ^ d

Tactic:
set y := q.den

Premises used: Rat.den
-- Module: Mathlib.Tactic.NormNum.Irrational
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
rwa rwa₁ rwa₂ rwa₃ : 0 ≤ q
⊢ 0 ≤ x'

Tactic:
rwa [Rat.num_nonneg]

Premises used: Rat.num_nonneg
-- Module: Mathlib.Tactic.NormNum.Irrational
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
neg : ∀ (x : ℕ) (hx' : x' = (↑x : ℤ)), False
⊢ False

Tactic:
obtain ⟨x, hx'⟩ := Int.eq_ofNat_of_zero_le (show 0 ≤ x' by rwa [Rat.num_nonneg])

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℤ)
⊢ HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d

Tactic:
rw [hx'] at h
-- Module: Mathlib.Tactic.NormNum.Irrational
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 : ℤ)
h₁ : HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) = HDiv.hDiv (α := ℚ) (↑(↑x : ℤ) : ℚ) (↑y : ℚ) ^ d
⊢ x' = (↑x : ℤ)

Tactic:
rw [hx'] at h