mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
⊢ termSum 1 N = log (↑N + 1) - ↑(harmonic (N + 1)) + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
⊢ mulHeight x = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
⊢ logHeight x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
⊢ vecCons 0 x ∘ ⇑e = Sum.elim x 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ HasSum (fun n ↦ term (n + 1) 1) (1 - γ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ ↑n ≤ ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
⊢ ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ term n s = ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ (s + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
⊢ mulHeight (vecCons 0 x) = mulHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
⊢ logHeight (vecCons 0 x) = logHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons 0 x)) = mulHeight (vecCons a x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ logHeight (vecCons a (vecCons 0 x)) = logHeight (vecCons a x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x))) = mulHeight (vecCons a (vecCons b x))

Tactic:
← mulHeight_comp_equiv (Equiv.swap (Fin.succ 0) (Fin.succ 1)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x)) ∘ ⇑(Equiv.swap (Fin.succ 0) (Fin.succ 1))) =
    mulHeight (vecCons a (vecCons b x))
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑1 = ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - λ ^ 2 * Y - ↑S.u₄ * (λ ^ 2 * Z)

Tactic:
← hY,

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑1 = ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (λ ^ 2 * Z)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons b (vecCons 0 x))) = mulHeight (vecCons a (vecCons b x))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ logHeight (vecCons a (vecCons b (vecCons 0 x))) = logHeight (vecCons a (vecCons b x))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
⊢ logHeight (c • x) = logHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ (s + 1) = ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-s) - ↑n * x ^ (-(s + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
i : Fin 2
⊢ v (![x, 1] i) = ![v x, 1] i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ max (v x) 1 = ⨆ i, v (![x, 1] i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : ∀ (v : AbsoluteValue K ℝ) (x : K), max (v x) 1 = ⨆ i, v (![x, 1] i)
⊢ ![x, 1] ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x = mulHeight ![x, 1]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ logHeight₁ x = logHeight ![x, 1]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-s) - ↑n * x ^ (-(s + 1)) =
    (∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-s)) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-(s + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑(-1) = -(↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - λ ^ 2 * Y - ↑S.u₄ * (λ ^ 2 * Z))

Tactic:
← hY,

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 + 1 = λ ^ 2 * Z
⊢ ↑S.u₄ - ↑(-1) = -(↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (λ ^ 2 * Z))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x / y) = logHeight ![x, y]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -s ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -(s + 1) ≠ -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ ↑(Nat.card ι) ^ totalWeight K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
v : AbsoluteValue K ℝ
⊢ ⨆ i, v ((x ^ n) i) = (⨆ i, v (x i)) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ^ n) i) = (⨆ i, v (x i)) ^ n
⊢ x ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
⊢ mulHeight (x ^ n) = mulHeight x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
⊢ logHeight (x ^ n) = ↑n * logHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ x • ![x⁻¹, 1] = ![1, x]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.u₄ = 1 ∨ S.u₄ = -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ logHeight₁ x⁻¹ = logHeight₁ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.u₄ ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ logHeight₁ (x ^ n) = ↑n * logHeight₁ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + (↑S.u₄ * S.Z) ^ 3 = S.Y ^ 3 + ↑S.u₄ ^ 2 * ↑S.u₄ * S.Z ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ ^ 2 * ↑S.u₄ * S.Z ^ 3 = S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (S.multiplicity - 1) * S.X = 0
⊢ S.X = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (A i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity - 1 = 0
⊢ 1 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ λ ^ (S.multiplicity - 1) * S.X

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ (S.multiplicity - 1) ∣ S.Solution'_descent.c

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
⊢ logHeight₁ (x ^ n) = ↑n.natAbs * logHeight₁ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n + 1) ^ (-(s + 1) + 1) - ↑n ^ (-(s + 1) + 1)) / (-(s + 1) + 1)) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
show -(s + 1) + 1 = -s by ring,

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n + 1) ^ (-s) - ↑n ^ (-s)) / -s) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun i ↦ (⨆ i_1, ↑i (A i_1)) * ⨆ i_1, ↑i (x i_1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Solution'_descent.multiplicity = S.multiplicity - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ (mulHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.multiplicity ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Solution'_descent.multiplicity < S.multiplicity

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
this : 0 ≤ logHeight A + logHeight x
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ ↑(Nat.card ι) ^ totalWeight K ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
this : ↑(Nat.card ι) ^ totalWeight K ≠ 0
⊢ 0 < mulHeight fun j ↦ ∑ i, A (j, i) * x i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: ⊢ FermatLastTheoremFor 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-s)) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-(s + 1)) =
    1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
⊢ term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
a : α
x✝ : a ∈ univ
⊢ (Multiset.map (fun i ↦ ⨆ i_1, i (x a i_1)) archAbsVal).prod * ∏ᶠ (a_1 : ↑nonarchAbsVal), ⨆ i, ↑a_1 (x a i) =
    mulHeight (x a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.EllipticCurve

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
⊢ ∃ C, ∀ (x : Fin 3 → K), |(logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x| ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ span {x} ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
⊢ t₀.Finite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ v ((eval x) p) ≤ (p.coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
⊢ t₁ ⊆ t₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (mulHeight fun I ↦ ∏ a, x a (I a)) = ∏ a, mulHeight (x a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (logHeight fun I ↦ ∏ a, x a (I a)) = ∑ a, logHeight (x a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ (fun a ↦ x a.1 * y a.2) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
⊢ t₂.Finite

Tactic:
by

Goal state after: