mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ P ∣ differentIdeal A B

Tactic:
suffices ∀ x ∈ a, Algebra.intTrace A B x ∈ p by
    have hP : ((P :)⁻¹ : FractionalIdeal B⁰ L) = a / p.map (algebraMap A B) := by
      apply inv_involutive.injective
      simp only [ha, FractionalIdeal.coeIdeal_mul, inv_div, mul_div_assoc]
      rw [div_self (by simpa), mul_one, inv_inv]
    rw [Ideal.dvd_iff_le, differentialIdeal_le_iff (K := K) (L := L) hPbot, hP,
      Submodule.map_le_iff_le_comap]
    intro x hx
    rw [Submodule.restrictScalars_mem, FractionalIdeal.mem_coe,
      FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp')] at hx
    rw [Submodule.mem_comap, LinearMap.coe_restrictScalars, ← FractionalIdeal.coe_one,
      ← div_self (G₀ := FractionalIdeal A⁰ K) (a := p) (by simpa using hp),
      FractionalIdeal.mem_coe, FractionalIdeal.mem_div_iff_of_ne_zero (by simpa using hp)]
    simp only [FractionalIdeal.mem_coeIdeal, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at hx
    intro y hy'
    obtain ⟨y, hy, rfl : algebraMap A K _ = _⟩ := (FractionalIdeal.mem_coeIdeal _).mp hy'
    obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
    have : Algebra.trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K) := by
      rw [← Algebra.algebraMap_intTrace (A := A)]
      exact ⟨Algebra.intTrace A B z, this z hz, rfl⟩
    rwa [mul_comm, ← smul_eq_mul, ← map_smul, Algebra.smul_def, mul_comm,
      ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']

Goal state after:
case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ ∀ x ∈ a, (intTrace A B) x ∈ p
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ ∀ x ∈ a, (intTrace A B) x ∈ p

Tactic:
intro x

Goal state after:
case neg
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
x : B
⊢ x ∈ a → (intTrace A B) x ∈ p
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case hgt
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ (1 + 1)
⊢ P ∣ differentIdeal A B

Tactic:
← pow_one P,

Goal state after:
case hgt
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ (1 + 1)
⊢ P ^ 1 ∣ differentIdeal A B
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 ![x, y] = mulHeight ![y, x]

Tactic:
rw [show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl]

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.Height.Basic

Goal state before:
pp: α : Type u_5
inst✝ : ConditionallyCompleteLattice α
a b : α
⊢ ∀ (c : α), a ⊔ b ≤ c ↔ iSup ![a, b] ≤ c

Tactic:
simp [ciSup_le_iff, Fin.forall_fin_two]

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 c) archAbsVal).prod * (Multiset.map (fun i ↦ ⨆ i_1, i (x i_1)) archAbsVal).prod *
      ((∏ᶠ (i : ↑nonarchAbsVal), ↑i c) * ∏ᶠ (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:
mul_mul_mul_comm,

Goal state after:
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 c) archAbsVal).prod * ∏ᶠ (i : ↑nonarchAbsVal), ↑i c) *
      ((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)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
intro x

Goal state after:
n : ℕ
hn : 0 < n
x : ℝ
⊢ x ∈ uIcc (↑n) (↑n + 1) → 0 < x
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
⊢ 1 ≤ mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · simp
  obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := ne_iff.mp hx
  have hx' : (x i)⁻¹ • x ≠ 0 := by simp [hi, hx]
  rw [← mulHeight_smul_eq_mulHeight _ <| inv_ne_zero hi, mulHeight_eq hx']
  refine one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun v _ ↦ ?_) ?_
  · refine Finite.le_ciSup_of_le i <| le_of_eq ?_
    simpa using (inv_mul_cancel₀ <| v.ne_zero_iff.mpr hi).symm
  · refine one_le_finprod fun v ↦ Finite.le_ciSup_of_le i ?_
    simp [inv_mul_cancel₀ <| v.val.ne_zero_iff.mpr hi]

Goal state after:
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
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
refine ⟨-1, X - Y - S.u₄ * Z, ?_⟩
    rw [show λ ^ 2 * (X - Y - S.u₄ * Z) = λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z) by ring,
      ← hX, ← hY, ← hZ, ← formula2]
    ring

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:
intro x

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
⊢ x ∈ uIcc (↑n) (↑n + 1) → 0 < x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr.inr.inr
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
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    ↑(Nat.card ι) ^ totalWeight K *
        ((map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) *
      ((map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i))

Tactic:
mul_mul_mul_comm,

Goal state after:
case inr.inr.inr.inr
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
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    ↑(Nat.card ι) ^ totalWeight K * (map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod *
      (((map (fun v ↦ ⨆ i, v (A i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) *
        ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i))
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:
mulHeight_eq ?h₁

Goal state after:
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (∏ a, x a (i a))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∏ a, x a (i a)) =
    ∏ a, mulHeight (x a)

case h₁
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
⊢ (fun I ↦ ∏ a, x a (I a)) ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
⊢ termSum s N =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp only [termSum]

Goal state after:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
| ∑ n ∈ Finset.range N, term (n + 1) s

Tactic:
2,

Goal state after:
N : ℕ
s : ℝ
hs : 1 < s
| fun n ↦ term (n + 1) s
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
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (x i.1 * y i.2)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i.1 * y i.2) =
    ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) *
      ((Multiset.map (fun v ↦ ⨆ i, v (y i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (y i))

Tactic:
mul_mul_mul_comm,

Goal state after:
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (x i.1 * y i.2)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i.1 * y i.2) =
    (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * (Multiset.map (fun v ↦ ⨆ i, v (y i)) archAbsVal).prod *
      ((∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (y i))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) * (↑(n + 1) ^ s)⁻¹

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
← div_eq_mul_inv

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) / ↑(n + 1) ^ s

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
2,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
2,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ a ∈ range k, Z (a + 1) * (μ - 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)

Tactic:
2,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (∏ a ∈ range k, Z (a + 1) * (μ - 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| ∏ a ∈ range k, Z (a + 1) * (μ - 1)

Tactic:
2,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| fun a ↦ Z (a + 1) * (μ - 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| ∑ x, χ x * ψ (1 - x)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| fun x ↦ χ x * ψ (1 - x)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| ∑ x, χ x + ∑ x, ψ (1 - x)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| ∑ x, ψ (1 - x)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| ∑ x, ψ (1 - x)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
| fun x ↦ ψ (1 - x)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
⊢ ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

Tactic:
intro x

Goal state after:
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
⊢ x ∈ univ \ {0, 1} → (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
| ∑ x, χ x * χ⁻¹ (1 - x)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
| fun x ↦ χ x * χ⁻¹ (1 - x)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ (x * (1 - x)⁻¹)

Tactic:
← div_eq_mul_inv

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ (x / (1 - x))
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
h✝ : IsEmpty ι'
p : ι' → MvPolynomial ι K
x✝ : ι → K
h : ∀ (k : ι), ∑ j, (eval x✝) (q (k, j)) * (eval x✝) (p j) = x✝ k ^ (M + N)
⊢ 1 * mulHeight x✝ ^ N ≤ mulHeight fun j ↦ (eval x✝) (p j)

Tactic:
by simp [mulHeight_eval_ge_aux p h]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x + ∑ x, χ x * φ (0 - x) * ψ 0

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x + ∑ x, χ x * φ (0 - x) * ψ 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x + ∑ x, χ x * φ (0 - x) * ψ 0

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| ∑ x, χ x * φ (0 - x) * ψ 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| ∑ x, χ x * φ (0 - x) * ψ 0

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
| fun x ↦ χ x * φ (0 - x) * ψ 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
| gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, (∑ x_1, χ x * (χ x_1 * (φ x * φ (1 - x_1)))) * ψ x

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
| ∑ x ∈ univ \ {0}, (∑ x_1, χ x * (χ x_1 * (φ x * φ (1 - x_1)))) * ψ x
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
| ∑ x ∈ univ \ {0}, (∑ x_1, χ x * (χ x_1 * (φ x * φ (1 - x_1)))) * ψ x

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
| fun x ↦ (∑ x_1, χ x * (χ x_1 * (φ x * φ (1 - x_1)))) * ψ x