mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight (![y, x] ∘ ⇑e) = mulHeight ![y, x]

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight (![y, x] ∘ ⇑e) = mulHeight ![y, x]
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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ λ ^ 2 * λ ^ (3 * S.multiplicity - 5) * ↑S.u₅ * S.X ^ 3 = λ ^ 2 * (λ ^ (3 * S.multiplicity - 5) * ↑S.u₅ * S.X ^ 3)

Tactic:
by ring

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
⊢ λ ^ 4 = λ ^ 2 * λ ^ 2

Tactic:
by ring

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ 0 ≤ ⨆ i, ↑v (x ↑i)

Tactic:
]

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ 0 ≤ ⨆ i, ↑v (x ↑i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
c : K
hc : c ≠ 0
⊢ mulHeight 0 = mulHeight 0

Tactic:
]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ (Multiset.map (fun i ↦ ⨆ i_1, i (x i_1)) archAbsVal).prod * ∏ᶠ (i : ↑nonarchAbsVal), ⨆ i_1, ↑i (x i_1) =
    (Multiset.map (fun i ↦ ⨆ i_1, i (x i_1)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
]

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

Goal state before:
pp: n : ℕ
s : ℝ
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume

Tactic:
]

Goal state after:
n : ℕ
s : ℝ
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (fun x ↦ (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (fun x ↦ (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntervalIntegrable (fun x ↦ (x - ↑n) / x ^ (s + 1)) volume (↑n) (↑n + 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)]

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (fun x ↦ (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ 1 ≤
    (Multiset.map (fun v ↦ ⨆ i_1, v (((x i)⁻¹ • x) i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i_1, ↑v (((x i)⁻¹ • x) i_1)

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ 1 ≤
    (Multiset.map (fun v ↦ ⨆ i_1, v (((x i)⁻¹ • x) i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i_1, ↑v (((x i)⁻¹ • x) i_1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 < x
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

pp: case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

pp: case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)

Tactic:
]

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

case hf
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (HDiv.hDiv 1) volume (↑n) (↑n + 1)

case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: f : Fin 2 → ℝ
⊢ iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)

Tactic:
]

Goal state after:
f : Fin 2 → ℝ
⊢ iSup ![f 0, f 1] = max (![f 0, f 1] 0) (![f 0, f 1] 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
⊢ v (l a + ∑ x ∈ s, l x) ≤ ⨆ i, v (l ↑i)

Tactic:
]

Goal state after:
case insert
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
⊢ v (l a + ∑ x ∈ s, l x) ≤ ⨆ i, v (l ↑i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
⊢ max (v (l a)) (⨆ i, v (l ↑i)) ≤ ⨆ i, v (l ↑i)

Tactic:
]

Goal state after:
case insert
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
⊢ max (v (l a)) (⨆ i, v (l ↑i)) ≤ ⨆ i, v (l ↑i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
]

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n = log (↑n + 1) - log ↑n

pp: case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

pp: case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

pp: case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

pp: case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1

Tactic:
]

Goal state after:
case e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n + 1 ≠ 0

case e_a.hy
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ↑n ≠ 0

case e_a.ha
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n

case e_a.hb
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ 0 < ↑n + 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ⨆ i, ⨆ (h : i ∈ Finset.univ), v (l ↑⟨i, h⟩) ≤ ⨆ i, v (l i)

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : FunLike F β ℝ
inst✝² : NonnegHomClass F β ℝ
inst✝¹ : ZeroHomClass F β ℝ
v : F
l : α → β
inst✝ : Fintype α
hv : IsNonarchimedean ⇑v
⊢ ⨆ i, ⨆ (h : i ∈ Finset.univ), v (l ↑⟨i, h⟩) ≤ ⨆ i, v (l i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x ^ 2)⁻¹ = (x ^ 2)⁻¹

pp: case e_a.e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ x

Tactic:
]

Goal state after:
case e_a.e_a.hx
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ x
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 - 1) - ↑S.u₄ * (S.Z ^ 3 - 1)

Tactic:
]

Goal state after:
case inl.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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 - 1) - ↑S.u₄ * (S.Z ^ 3 - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -1 < -2 ∨ -2 ≠ -1 ∧ 0 ∉ uIcc (↑n) (↑n + 1)

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -1 < -2 ∨ -2 ≠ -1 ∧ 0 ∉ uIcc (↑n) (↑n + 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, v (A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, v (A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (Sum.elim x 0 i) =
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
]

Goal state after:
case inr
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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (Sum.elim x 0 i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (Sum.elim x 0 i) =
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, (⨆ ji, v (A ji)) * ⨆ i, v (x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

pp: case h
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
i : ι
x✝ : i ∈ Finset.univ
⊢ v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ∑ i, (⨆ ji, v (A ji)) * ⨆ i, v (x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

case h
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
i : ι
x✝ : i ∈ Finset.univ
⊢ v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ↑(Fintype.card ι) * ((⨆ ji, v (A ji)) * ⨆ i, v (x i)) ≤ ↑(Fintype.card ι) * ((⨆ ji, v (A ji)) * ⨆ i, v (x i))

Tactic:
]

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

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
⊢ ⨆ i, v (A (j, ↑i) * x ↑i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
]

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
⊢ ⨆ i, v (A (j, ↑i) * x ↑i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
⊢ ⨆ i, v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
]

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
⊢ ⨆ i, v (A (j, i)) * v (x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inl.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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 - 1) - ↑S.u₄ * (S.Z ^ 3 + 1))

Tactic:
]

Goal state after:
case inl.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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 - 1) - ↑S.u₄ * (S.Z ^ 3 + 1))
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
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
hx : x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0
⊢ mulHeight (Sum.elim (fun i ↦ x ↑i) 0) = mulHeight fun i ↦ x ↑i

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
hx : x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0
⊢ mulHeight (Sum.elim (fun i ↦ x ↑i) 0) = mulHeight fun i ↦ x ↑i
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑(N + 1) + 1) - log ↑(N + 1) - 1 / (↑(N + 1) + 1)) =
    log (↑(N + 1) + 1) - ↑(harmonic (N + 1) + (↑(N + 1 + 1))⁻¹) + 1

Tactic:
]

Goal state after:
case succ
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ log (↑N + 1) - ↑(harmonic (N + 1)) + 1 + (log (↑(N + 1) + 1) - log ↑(N + 1) - 1 / (↑(N + 1) + 1)) =
    log (↑(N + 1) + 1) - ↑(harmonic (N + 1) + (↑(N + 1 + 1))⁻¹) + 1
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 * 1 * 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
]

Goal state after:
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 * 1 * 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight ((x i)⁻¹ • x) = 1

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight ((x i)⁻¹ • x) = 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))

Tactic:
]

Goal state after:
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 < x
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 ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight x = mulHeight x

Tactic:
]

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) ∘ ⇑(Equiv.swap 0 1)) = mulHeight (vecCons a x)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a : K
x : Fin n → K
⊢ mulHeight (vecCons a (vecCons 0 x) ∘ ⇑(Equiv.swap 0 1)) = mulHeight (vecCons a x)
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) ∘ ⇑(Equiv.swap 0 1))) = mulHeight (vecCons a (vecCons b x))

Tactic:
]

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 0 1))) = mulHeight (vecCons a (vecCons b x))
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 : ℝ
hx : x ∈ uIcc (↑n) (↑n + 1)
⊢ (x ^ s)⁻¹ - ↑n * (x ^ s * x)⁻¹ = (x ^ s)⁻¹ - ↑n * (x ^ s * x)⁻¹

Tactic:
]

Goal state after:
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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (S.Z ^ 3 - 1)

Tactic:
]

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.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 - (S.Y ^ 3 + 1) - ↑S.u₄ * (S.Z ^ 3 - 1)
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)) =
    (∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-s)) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-(s + 1))

pp: case hf
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-s)) volume (↑n) (↑n + 1)

pp: case hg
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * x ^ (-(s + 1))) volume (↑n) (↑n + 1)

Tactic:
]

Goal state after:
case hf
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-s)) volume (↑n) (↑n + 1)

case hg
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * x ^ (-(s + 1))) volume (↑n) (↑n + 1)