mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : Additive (𝓞 K)ˣ
⊢ (fun w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul (x✝¹ + x✝))))) =
    (fun w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝¹)))) + fun w ↦
      ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(Additive.toMul x✝)))

Tactic:
simp [Real.log_mul, mul_add]; rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
by_cases hw : w = w₀
    · suffices -mult w₀ * Real.log (w₀ (x : K)) = 0 by
        rw [neg_mul, neg_eq_zero, ← hw] at this
        exact mult_log_place_eq_zero.mp this
      rw [← sum_logEmbedding_component, sum_eq_zero]
      exact fun w _ ↦ congrFun h w
    · exact mult_log_place_eq_zero.mp (congrFun h ⟨w, hw⟩)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ‖(logEmbedding K) x‖ ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r

Tactic:
Pi.norm_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
w : { w // w ≠ w₀ }
r : NNReal
h : ↑(univ.sup fun b ↦ ‖(logEmbedding K) x b‖₊) ≤ ↑r
⊢ |(logEmbedding K) (Additive.ofMul x) w| ≤ ↑r
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case neg.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ r ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
nth_rw 1 [← one_mul r]

Goal state after:
case neg.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : ¬w = w₀
hyp : ↑(↑⟨w, hw⟩).mult * |Real.log (↑⟨w, hw⟩ ((algebraMap (𝓞 K) K) ↑(Additive.ofMul x)))| ≤ r
⊢ 1 * r ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ #univ ≤ #{0, 1, -1}

Tactic:
have : Nontrivial R := by
      refine Fintype.one_lt_card_iff_nontrivial.1 ?_
      rw [h]
      simp
    rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]
    · rw [mem_singleton]
      intro H
      rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H
      apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H
      simp only [map_ofNat, map_zero] at H
      replace H : ((2 : ℕ) : ZMod 3) = 0 := H
      rw [natCast_eq_zero_iff] at H
      norm_num at H
    · simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ ∑ x ∈ univ.erase w, |v w x| < |v w w|

Tactic:
← sub_pos,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - ∑ x ∈ univ.erase w, |v w x|
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1))

Tactic:
by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1)) = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
rw [hy]; ring

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ 0 = quadraticCharFun F a * 0

Tactic:
mul_zero

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : b = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case neg.refine_1.mem
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
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x✝ : B
hxQ : x✝ ∈ Q
hx✝ : (intTrace A B) x✝ ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
z : A
hz : (algebraMap A K) z = ((traceForm K L) x) 1
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) ((algebraMap A B) y)) ∈ ↑p

Tactic:
simp only [Algebra.traceForm_apply, mul_one] at hz

Goal state after:
case neg.refine_1.mem
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
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x✝ : B
hxQ : x✝ ∈ Q
hx✝ : (intTrace A B) x✝ ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
z : A
hz : (algebraMap A K) z = (Algebra.trace K L) x
⊢ (Algebra.trace K L) (x * (Algebra.linearMap B L) ((algebraMap A B) y)) ∈ ↑p
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
h3a : 3 ∣ a
Hgcd : {a, b, c}.gcd id = 1
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ {a, b, c}.gcd id = 1

Tactic:
simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← Int.abs_eq_normalize]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ^ 2 = b ^ 2 ↔ a✝ ∈ {b, -b}

Tactic:
mem_insert,

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ^ 2 = b ^ 2 ↔ a✝ = b ∨ a✝ ∈ {-b}
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
have h := quadraticChar_card_card hF (ne_of_eq_of_ne (ringChar_zmod_n p) hp₁)
    (ne_of_eq_of_ne (ringChar_zmod_n p) hp₂.symm)

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h :
  (quadraticChar F) ↑(Fintype.card (ZMod p)) = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inl
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : p ≠ 2
inst✝ : Fact (Nat.Prime p)
hq : p ≠ 2
⊢ 0 = (-1) ^ (p / 2 * (p / 2)) * 0

Tactic:
mul_zero

Goal state after:
case inl
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : p ≠ 2
inst✝ : Fact (Nat.Prime p)
hq : p ≠ 2
⊢ 0 = 0
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p) ^ 2 - b ^ 2 = (b ^ p + b) * (b ^ p - b)

Tactic:
by rw [Nat.sq_sub_sq]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
⊢ (A * B).FermatPsp b

Tactic:
have hi_bpowpsubone : 1 ≤ b ^ (p - 1) := Nat.one_le_pow (p - 1) b hi_b

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
⊢ (A * B).FermatPsp b
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 : IsCoprime 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
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ a :=
  let __spread.0 := (Ideal.quotEquivOfEq ha).trans (P.quotientMulEquivQuotientProd a hPa);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
hx' : (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 = 0
⊢ (Algebra.trace (A ⧸ p) ((B ⧸ P) × B ⧸ a)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)) = 0

Tactic:
Algebra.trace_prod_apply,

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 : IsCoprime 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
hx : x ∈ a
this✝² : Algebra (A ⧸ p) (B ⧸ a) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝¹ : IsScalarTower A (A ⧸ p) (B ⧸ a)
this✝ : Module.Finite (A ⧸ p) (B ⧸ a)
this : Prime P
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ a :=
  let __spread.0 := (Ideal.quotEquivOfEq ha).trans (P.quotientMulEquivQuotientProd a hPa);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
hx' : (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 = 0
⊢ (Algebra.trace (A ⧸ p) (B ⧸ P)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).1 +
      (Algebra.trace (A ⧸ p) (B ⧸ a)) (e ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) p)) x)).2 =
    0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ ↑(η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 * (λ * ↑S.u₂ * ↑η) =
    S.X ^ 3 * ↑S.u₁ * λ ^ (3 * S.multiplicity - 2)

Tactic:
calc _ = S.X^3 *(S.u₂*S.u₂⁻¹)*(η^3*S.u₁)*(λ^((S.multiplicity-1)*3)*λ) := by push_cast; ring
    _ = S.X^3*S.u₁*λ^(3*S.multiplicity-2) := by simp [hζ.toInteger_cube_eq_one, ← pow_succ, this]

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

Goal state before:
pp: case insert.refine_2
α : 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)
⊢ ⨆ i, v (l ↑i) ≤ ⨆ i, v (l ↑i)

Tactic:
rcases isEmpty_or_nonempty s with hs | hs
      · simpa using Real.iSup_nonneg_of_nonnegHomClass v _
      exact ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

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 : ι'
⊢ v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
grw [hv.apply_sum_le]

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

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

Tactic:
simpa [this] using max_eq_iSup (v x) 1

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
i : ι
⊢ (↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = v ↑(x i)

Tactic:
rw [← mul_eq_one_iff_inv_eq₀ h.ne', mul_comm, Nat.cast_pow]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
i : ι
⊢ v ↑(x i) * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x 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 ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · rcases eq_or_ne (fun j ↦ constantCoeff (p j)) 0 with h | h
    · simp [h]
    · simpa using le_max_of_le_left <| mulHeight_constantCoeff_le_mulHeightBound h
  rcases eq_or_ne (fun j ↦ eval x (p j)) 0 with h₀ | h₀
  · grw [← le_max_right]
    simpa [h₀, mulHeight_zero] using one_le_pow₀ <| one_le_mulHeight x
  have H₀ (v : AbsoluteValue K ℝ) : 0 ≤ ⨆ j, (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c :=
    iSup_nonneg (fun j ↦ sum_nonneg' <| fun s ↦ by positivity)
  -- The following four statements are used in the `gcongr`s below.
  have H₁ :
     0 ≤ (archAbsVal.map (fun v ↦ ⨆ j, (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c)).prod :=
    prod_map_nonneg fun v _ ↦ H₀ v
  have H₂ : 0 ≤ (archAbsVal.map (fun v ↦ ⨆ i, v (x i))).prod :=
    prod_map_nonneg fun _ _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
  have H₃ : 0 ≤ ∏ᶠ v : nonarchAbsVal, ⨆ i, v.val ((eval x) (p i)) :=
    finprod_nonneg fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
  have H₄ : 0 ≤ ∏ᶠ v : nonarchAbsVal, ⨆ i, v.val (x i) :=
    finprod_nonneg fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..
  -- The following two statements are helpful for discharging the goals left by `gcongr`.
  have HH₁ (v : AbsoluteValue K ℝ) : 0 ≤ (⨆ i, v (x i)) ^ N :=
    pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass v _) N
  have HH₂ (f : ι' → ℝ) (j : ι') : f j ≤ ⨆ j, f j := Finite.le_ciSup ..
  simp only [mulHeight_eq hx, mulHeight_eq h₀, mulHeightBound_eq]
  grw [← le_max_left]
  rw [mul_pow, mul_mul_mul_comm]
  gcongr
  · -- archimedean part: reduce to "local" statement `eval_mvPolynomial_le`
    rw [← prod_map_pow, ← prod_map_mul]
    refine prod_map_le_prod_map₀ _ _ (fun _ _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
      fun v _ ↦ Real.iSup_le (fun j ↦ ?_) <| mul_nonneg (H₀ v) (HH₁ v)
    grw [v.eval_mvPolynomial_le (hp j) x]
    gcongr
    · exact HH₁ v
    · exact HH₂ (fun j ↦ (AddMonoidAlgebra.coeff <| p j).sum fun _ c ↦ v c) j
  · -- nonarchimedean part: reduce to "local" statement `eval_mvPolynomial_le`
    have := (Function.ne_iff.mp h₀).nonempty
    have F := hasFiniteMulSupport_iSup_nonarchAbsVal hx
    rw [finprod_pow F, ← finprod_mul_distrib (by fun_prop) (by fun_prop)]
    refine finprod_le_finprod (by fun_prop)
      (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
      (fun j ↦ ?_) ?_
    · grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
      gcongr
      · exact HH₁ v.val
      · grw [← HH₂, ← le_max_left]
    · exact mul_nonneg (iSup_nonneg fun _ ↦ by positivity) <| by simp only [HH₁]

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

Goal state before:
pp: case refine_4
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
y : F
hy : ¬-1 = y
⊢ y / (1 + y) / (1 - y / (1 + y)) = y

Tactic:
neg_eq_iff_eq_neg,

Goal state after:
case refine_4
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
y : F
hy : ¬1 = -y
⊢ y / (1 + y) / (1 - y / (1 + y)) = y
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 * ψ x * ∑ i, χ i * φ (1 - i)

Tactic:
← jacobiSum,

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
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, (χ * φ) x * ψ x * jacobiSum χ φ
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: 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 ^ (Module.finrank ℚ K - 1)
⊢ ∃ n, n ≠ 0 ∧ ↑n ≤ mulHeight₁ x ∧ IsIntegral ℤ (↑n * x)

Tactic:
refine ⟨n, hn, ?_, ha₁ ▸ a.isIntegral_coe⟩

Goal state after:
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 ^ (Module.finrank ℚ K - 1)
⊢ ↑n ≤ mulHeight₁ x
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')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)

Tactic:
let φ' := φ.ringHomComp (algebraMap F' FF')

Goal state after:
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')
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hf : 1 ≤ v (↑(x i) * ↑(f i))
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
map_mul

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hf : 1 ≤ v ↑(x i) * v ↑(f i)
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
⊢ minpoly R x = (powerBasis' hx').minpolyGen

Tactic:
adjoin.powerBasis',

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
⊢ minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ ^ orderOf χ = χ (-1) * ↑(Fintype.card F) * ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)

Tactic:
have := gaussSum_pow_eq_prod_jacobiSum_aux χ ψ (n := orderOf χ - 1) (by lia) (by lia)
  apply_fun (gaussSum χ ψ * ·) at this
  rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos (by lia)] at this
  have hχ₁ : χ ≠ 1 :=
    fun h ↦ ((orderOf_one (G := MulChar F R) ▸ h ▸ hχ).trans_lt Nat.one_lt_two).false
  rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]

Goal state after: