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

Goal state before:
pp: case e_a.e_f
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
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)

pp: case e_a
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
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, ↑v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_1)

Tactic:
<;>

Goal state after:
case e_a.e_f
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
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)

case e_a
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
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (fun v ↦ ⨆ i, ↑v (x i.1 * y i.2)) = fun i ↦ (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ (mulHeight fun j ↦ constantCoeff (p j)) ≤ mulHeightBound p

Tactic:
simp only [mulHeight_eq h, mulHeightBound_eq]
  gcongr
  · exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..
  · exact prod_map_nonneg fun v _ ↦ iSup_nonneg fun _ ↦ sum_nonneg fun _ _ ↦ by positivity
  · have H (v : AbsoluteValue K ℝ) (j : ι') :
        v (constantCoeff (p j)) ≤ (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c :=
      single_eval_le_sum _ v.map_zero (fun _ ↦ by positivity) _
    exact prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Finite.ciSup_mono (H v)
  · have := (Function.ne_iff.mp h).nonempty
    refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_
    refine fun v ↦ Finite.ciSup_mono fun j ↦ ?_
    rw [show constantCoeff (p j) = coeff 0 (p j) from rfl]
    rcases eq_or_ne (coeff 0 (p j)) 0 with h₀ | h₀
    · simp [h₀]
    · exact le_sup_of_le_left <| Finite.le_ciSup_of_le ⟨0, by simp [h₀]⟩ le_rfl

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⋯
this : Nonempty { j // ↑(x j) ≠ 0 }
x✝ : ι
⊢ ↑(x x✝) ≠ 0 ↔ x✝ ∈ Function.support x

pp: case e'_3.h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⋯
this : Nonempty { j // ↑(x j) ≠ 0 }
e_2✝ : { j // ↑(x j) ≠ 0 } = ↑(Function.support x)
a✝¹ : { j // ↑(x j) ≠ 0 }
a'✝ : ↑(Function.support x)
a✝ : a✝¹ ≍ a'✝
x✝ : ι
⊢ ↑(x x✝) ≠ 0 ↔ x✝ ∈ Function.support x

Tactic:
<;>

Goal state after:
case e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⋯
this : Nonempty { j // ↑(x j) ≠ 0 }
x✝ : ι
⊢ ↑(x x✝) ≠ 0 ↔ x✝ ∈ Function.support x

case e'_3.h.e'_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⋯
this : Nonempty { j // ↑(x j) ≠ 0 }
e_2✝ : { j // ↑(x j) ≠ 0 } = ↑(Function.support x)
a✝¹ : { j // ↑(x j) ≠ 0 }
a'✝ : ↑(Function.support x)
a✝ : a✝¹ ≍ a'✝
x✝ : ι
⊢ ↑(x x✝) ≠ 0 ↔ x✝ ∈ Function.support x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case e'_2.e'_5.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

pp: case e'_2.e'_5.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)

pp: case e'_2.e'_5.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

pp: case e'_2.e'_5.«3»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case e'_2.e'_5.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.e'_5.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)

case e'_2.e'_5.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.e'_5.«3»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous 1

pp: case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous 1

pp: case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous 1

Tactic:
<;>

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous 1

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous 1

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case h₂.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case h₂.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case h₂.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩))

case h₂.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e'_5
⊢ riemannZeta₀ 1 = ↑γ

pp: case right.convert_2
⊢ ∀ x ∈ {1}ᶜ, riemannZeta x - 1 / (x - 1) = riemannZeta₀ x

Tactic:
<;>

Goal state after:
case e'_5
⊢ riemannZeta₀ 1 = ↑γ

case right.convert_2
⊢ ∀ x ∈ {1}ᶜ, riemannZeta x - 1 / (x - 1) = riemannZeta₀ x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case e'_3.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨0, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case e'_3.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨1, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case e'_3.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨2, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨2, ⋯⟩))

Tactic:
<;>

Goal state after:
case e'_3.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨0, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨0, ⋯⟩))

case e'_3.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨1, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨1, ⋯⟩))

case e'_3.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨2, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hx
s : ℝ
hs : s > 1
this : (riemannZeta ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re
⊢ (s - 1)⁻¹ ≠ 0

pp: case hy
s : ℝ
hs : s > 1
this : (riemannZeta ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re
⊢ (riemannZeta₁ ↑s).re ≠ 0

Tactic:
<;>

Goal state after:
case hx
s : ℝ
hs : s > 1
this : (riemannZeta ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re
⊢ (s - 1)⁻¹ ≠ 0

case hy
s : ℝ
hs : s > 1
this : (riemannZeta ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re
⊢ (riemannZeta₁ ↑s).re ≠ 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      (jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
rw [mul_mul_mul_comm, jacobiSum_mul_nontrivial Hχφ, mul_inv, ← ringHomComp_inv,
    ← ringHomComp_inv, jacobiSum_mul_nontrivial Hχφ', map_natCast, ← mul_mul_mul_comm,
    gaussSum_mul_gaussSum_eq_card Hχ ψ.prim, gaussSum_mul_gaussSum_eq_card Hφ ψ.prim,
    ← mul_inv, gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
x : 𝓞 K
hx : x ∈ {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
⊢ ↑x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : a ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}
⊢ a ∈ RingOfIntegers.val '' {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
x : 𝓞 K
hx : x ∈ {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
⊢ ↑x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : a ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}
⊢ a ∈ RingOfIntegers.val '' {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
<;>

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case e'_2.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case e'_2.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨1, ⋯⟩)