awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
rwa : ¬¬p ∣ N
rwa₁ rwa₂ rwa₃ rwa₄ : p ∣ N
⊢ ¬IsUnit (M := ZMod N) (↑p : ZMod N)

Tactic:
rwa [ZMod.isUnit_prime_iff_not_dvd h, not_not]

Premises used: Classical.not_not, ZMod.isUnit_prime_iff_not_dvd
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ ¬IsUnit (M := ZMod N) (↑p : ZMod N)

Tactic:
have : ¬IsUnit (p : ZMod N) := by rwa [ZMod.isUnit_prime_iff_not_dvd h, not_not]
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
pos :
  1 =
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))
⊢ (1 -
        HMul.hMul (α := ℂ)
          ((((changeLevel hMN : (a : DirichletCharacter ℂ M) → DirichletCharacter ℂ N) χ : DirichletCharacter ℂ N) :
                (a : ZMod N) → ℂ)
              (↑p : ZMod N) :
            ℂ)
          (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ =
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
rw [MulChar.map_nonunit _ this, zero_mul, sub_zero, inv_one]

Premises used: inv_one, sub_zero, MulZeroClass.zero_mul, MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
⊢ 1 =
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
(inv_mul_cancel₀ ?_).symm

Premises used: Eq.symm, inv_mul_cancel₀
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
pos : 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)) ≠ 0
⊢ 1 =
    (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))⁻¹ *
      (1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)))

Tactic:
refine (inv_mul_cancel₀ ?_).symm

Premises used: Eq.symm, inv_mul_cancel₀
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
pos : HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)) ≠ 1
⊢ 1 - HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)) ≠ 0

Tactic:
rw [sub_ne_zero, ne_comm]

Premises used: sub_ne_zero, ne_comm
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
apply_fun :
  Ne (α := ℝ)
    ((fun (x : ℂ) ↦ ‖x‖)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    ((fun (x : ℂ) ↦ ‖x‖) 1)
⊢ HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s)) ≠ 1

Tactic:
apply_fun (‖·‖)

Premises used: Norm.norm
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
simp : norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) * ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≠ 1
⊢ Ne (α := ℝ)
    ((fun (x : ℂ) ↦ ‖x‖)
      (HMul.hMul (α := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) (HPow.hPow (α := ℂ) (↑p : ℂ) (-s))))
    ((fun (x : ℂ) ↦ ‖x‖) 1)

Tactic:
simp only [norm_mul, norm_one]

Premises used: NormOneClass.norm_one, norm_mul
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
⊢ norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) ≤ 1

Tactic:
have ha : ‖χ p‖ ≤ 1 := χ.norm_le_one p
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
ha : norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) ≤ 1
⊢ ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≤ 1 / 2

Tactic:
have hb : ‖(p : ℂ) ^ (-s)‖ ≤ 1 / 2 := norm_prime_cpow_le_one_half ⟨p, h⟩ hs
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
ha : norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) ≤ 1
hb : ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≤ 1 / 2
⊢ 1 * (1 / 2) < 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries
Goal:
M N : ℕ
inst : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this_1 : ∀ (f : Primes → ℂ), Eq (α := ℂ) (∏' (p : Primes), f p) (∏' (p : (↑{p : ℕ | Nat.Prime p} : Type)), f p)
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit (M := ZMod N) (↑p : ZMod N)
ha : norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) ≤ 1
hb : ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≤ 1 / 2
⊢ norm (E := ℂ) ((χ : (a : ZMod M) → ℂ) (↑p : ZMod M) : ℂ) * ‖HPow.hPow (α := ℂ) (↑p : ℂ) (-s)‖ ≠ 1

Tactic:
exact ((mul_le_mul ha hb (norm_nonneg _) zero_le_one).trans_lt (by norm_num)).ne

Premises used: zero_le_one, mul_le_mul, LE.le.trans_lt, norm_nonneg, LT.lt.ne
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ HSub.hSub (α := ℂ) 1 0 ∈ slitPlane

Tactic:
have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
this funProp : HSub.hSub (α := ℂ) 1 0 ∈ slitPlane
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0

Tactic:
have hg : DifferentiableAt ℂ (fun z ↦ log (1 - z)) 0 := by
    have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane
    fun_prop
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0
⊢ Asymptotics.IsBigO (E := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 - z)) id

Tactic:
simpa only [sub_zero, log_one] using hg.isBigO_sub

Premises used: Complex.log_one, sub_zero, DifferentiableAt.isBigO_sub
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0
⊢ Asymptotics.IsBigO (E := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 - z)) id

Tactic:
have : (fun z ↦ log (1 - z)) =O[𝓝 0] id := by
    simpa only [sub_zero, log_one] using hg.isBigO_sub
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0
this : Asymptotics.IsBigO (E := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 - z)) id
⊢ Summable (α := ℂ) fun (n : α) ↦ log (1 - f n)

Tactic:
this.comp_summable hsum

Premises used: Complex.log, Asymptotics.IsBigO.comp_summable
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ log (1 - z)) 0
this : Asymptotics.IsBigO (E := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 - z)) id
⊢ Summable (α := ℂ) fun (n : α) ↦ log (1 - f n)

Tactic:
exact this.comp_summable hsum

Premises used: Asymptotics.IsBigO.comp_summable
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
⊢ ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1

Tactic:
have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
hs : ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1
⊢ ∀ (p : Nat.Primes), HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ) ≠ 0

Tactic:
have hp (p : Nat.Primes) : 1 - f p ≠ 0 :=
    fun h ↦ (norm_one (α := ℂ) ▸ (sub_eq_zero.mp h) ▸ hs p.prop.one_lt).false
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
hs : ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1
hp : ∀ (p : Nat.Primes), HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ) ≠ 0
⊢ ∏' (b : Subtype Nat.Prime),
      (cexp ∘
          (fun (b : ℕ) ↦ -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) b : ℂ))) ∘
            Subtype.val (p := Nat.Prime))
        b =
    cexp
      (∑' (b : Subtype Nat.Prime),
        ((fun (b : ℕ) ↦ -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) b : ℂ))) ∘
            Subtype.val (p := Nat.Prime))
          b)

Tactic:
have H := hsum.of_norm.clog_one_sub.neg.subtype Nat.Prime |>.hasSum.cexp.tprod_eq
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
hs : ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1
hp : ∀ (p : Nat.Primes), HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ) ≠ 0
H :
  ∏' (b : Subtype Nat.Prime),
      (cexp ∘
          (fun (b : ℕ) ↦ -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) b : ℂ))) ∘
            Subtype.val (p := Nat.Prime))
        b =
    cexp
      (∑' (b : Subtype Nat.Prime),
        ((fun (b : ℕ) ↦ -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) b : ℂ))) ∘
            Subtype.val (p := Nat.Prime))
          b)
⊢ ∏' (b : Subtype Nat.Prime), (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ))⁻¹ =
    cexp (∑' (b : Subtype Nat.Prime), -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ)))

Tactic:
simp only [Function.comp_apply, exp_neg, exp_log (hp _)] at H

Premises used: Complex.exp_neg, Function.comp_apply, Complex.exp_log
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
hs : ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1
hp : ∀ (p : Nat.Primes), HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ) ≠ 0
H :
  ∏' (b : Subtype Nat.Prime), (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ))⁻¹ =
    cexp (∑' (b : Subtype Nat.Prime), -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ)))
⊢ cexp (∑' (p : Nat.Primes), -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ))) =
    ∑' (n : ℕ), (f : (a : ℕ) → ℂ) n

Tactic:
H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum

Premises used: EulerProduct.eulerProduct_completely_multiplicative_tprod, Nat.Primes, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.EulerProduct.ExpLog
Goal:
f : ℕ →*₀ ℂ
hsum : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((f : (a : ℕ) → ℂ) x : ℂ)
hs : ∀ {p : ℕ} (hp : 1 < p), norm (E := ℂ) ((f : (a : ℕ) → ℂ) p : ℂ) < 1
hp : ∀ (p : Nat.Primes), HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ) ≠ 0
H :
  ∏' (b : Subtype Nat.Prime), (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ))⁻¹ =
    cexp (∑' (b : Subtype Nat.Prime), -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑b : ℕ) : ℂ)))
⊢ cexp (∑' (p : Nat.Primes), -log (HSub.hSub (α := ℂ) (β := ℂ) (1 : ℂ) ((f : (a : ℕ) → ℂ) (↑p : ℕ) : ℂ))) =
    ∑' (n : ℕ), (f : (a : ℕ) → ℂ) n

Tactic:
exact H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum

Premises used: EulerProduct.eulerProduct_completely_multiplicative_tprod, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
x x_1 x_2 : ℕ
h : x ≠ 0
h_1 : x_1 ≠ 0
h_2 : x_2 ≠ 0
⊢ HPow.hPow (β := ℕ) x 0 + HPow.hPow (β := ℕ) x_1 0 ≠ HPow.hPow (β := ℕ) x_2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 1
⊢ Ne (α := ℕ) 1 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 1
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 1
⊢ HPow.hPow (α := ℕ) (β := ℕ) 1 1 + HPow.hPow (α := ℕ) (β := ℕ) 1 1 = HPow.hPow (α := ℕ) (β := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 2
⊢ Ne (α := ℕ) 3 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 2
⊢ Ne (α := ℕ) 4 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 2
⊢ Ne (α := ℕ) 5 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
h : FermatLastTheoremFor 2
⊢ HPow.hPow (α := ℕ) (β := ℕ) 3 2 + HPow.hPow (α := ℕ) (β := ℕ) 4 2 = HPow.hPow (α := ℕ) (β := ℕ) 5 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
obtain : ∀ (k : ℕ), a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
obtain ⟨k, rfl⟩ := hmn

Premises used: rfl
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
simp_rw : (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m
⊢ a ^ (m * k) + b ^ (m * k) ≠ c ^ (m * k)

Tactic:
simp_rw [pow_mul']

Premises used: pow_mul'
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m

Tactic:
hm _ _ _ ?_ ?_ ?_
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
refine_1 : a ^ k ≠ 0
refine_2 : b ^ k ≠ 0
refine_3 : c ^ k ≠ 0
⊢ (a ^ k) ^ m + (b ^ k) ^ m ≠ (c ^ k) ^ m

Tactic:
refine hm _ _ _ ?_ ?_ ?_
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ k ≠ 0

Tactic:
pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ a ^ k ≠ 0

Tactic:
exact pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ b ^ k ≠ 0

Tactic:
pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ b ^ k ≠ 0

Tactic:
exact pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ c ^ k ≠ 0

Tactic:
pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
m : ℕ
hm : FermatLastTheoremWith R m
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
k : ℕ
⊢ c ^ k ≠ 0

Tactic:
exact pow_ne_zero _ ‹_›

Premises used: pow_ne_zero
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremFor m
⊢ FermatLastTheoremFor n

Tactic:
FermatLastTheoremWith.mono hmn hm

Premises used: FermatLastTheoremWith.mono, FermatLastTheoremFor
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremFor m
⊢ FermatLastTheoremFor n

Tactic:
exact FermatLastTheoremWith.mono hmn hm

Premises used: FermatLastTheoremWith.mono
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremWith ℕ n

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ FermatLastTheoremWith ℤ n

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
⊢ ∀ (a : FermatLastTheoremWith ℕ n), FermatLastTheoremWith ℤ n

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
inl : ∀ (hn : Even n), False
inr : ∀ (hn : Odd n), False
⊢ False

Tactic:
obtain hn | hn := n.even_or_odd

Premises used: Nat.even_or_odd
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ b.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ c.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
inl : Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)

Premises used: Int.natAbs, Iff.mp, Int.natCast_inj
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
inl : |a| ^ n + |b| ^ n = |c| ^ n
⊢ Eq (α := ℤ) (↑(a.natAbs ^ n + b.natAbs ^ n) : ℤ) (↑(c.natAbs ^ n) : ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Tactic:
simp only [hn.pow_abs, habc]

Premises used: Even.pow_abs
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
inr : ∀ (ha : a < 0), False
inr₁ : ∀ (ha : 0 < a), False
⊢ False

Tactic:
obtain ha | ha := ha.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
inr : ∀ (hb : b < 0), False
inr₁ : ∀ (hb : 0 < b), False
⊢ False

Tactic:
obtain hb | hb := hb.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
inr : ∀ (hb : b < 0), False
inr₁ : ∀ (hb : 0 < b), False
⊢ False

Tactic:
obtain hb | hb := hb.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
inr : ∀ (hc : c < 0), False
inr₁ : ∀ (hc : 0 < c), False
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
inr : ∀ (hc : c < 0), False
inr₁ : ∀ (hc : 0 < c), False
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
inr : ∀ (hc : c < 0), False
inr₁ : ∀ (hc : 0 < c), False
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
inr : ∀ (hc : c < 0), False
inr₁ : ∀ (hc : 0 < c), False
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ a.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ b.natAbs ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FLT.Basic
Goal:
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha_1 : a ≠ 0
hb_1 : b ≠ 0
hc_1 : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ c.natAbs ≠ 0

Tactic:
positivity