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

Goal state before:
pp: case e_a.coprime
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
this✝⁵ : NumberField K
this✝⁴ : NeZero n₁
this✝³ : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this✝² : IsCyclotomicExtension {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this✝¹ : IsCyclotomicExtension {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this✝ : IsGalois ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤
h_cpr : IsCoprime (NumberField.discr ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : ℚ⟮ζ ^ n₂⟯.LinearDisjoint ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
this : ∀ {n p : ℕ}, p ∈ n.primeFactors → p - 1 ∣ φ n
⊢ n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      ((∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1))) * ∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    (n₁ * n₂) ^ (φ n₁ * φ n₂) /
      ((∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1))) * ∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))

Tactic:
rw [mul_pow, mul_comm n₂.totient]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ =
    (dual B (FractionRing B) 1)⁻¹ * (extendedHom (FractionRing C) C) (dual A (FractionRing A) 1)⁻¹

Tactic:
map_inv₀,

Goal state after:
A : Type u_1
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : IsDomain A
inst✝¹⁴ : IsIntegrallyClosed A
inst✝¹³ : IsDedekindDomain B
inst✝¹² : IsTorsionFree A B
C : Type u_3
inst✝¹¹ : IsDomain B
inst✝¹⁰ : CommRing C
inst✝⁹ : Algebra B C
inst✝⁸ : Algebra A C
inst✝⁷ : IsDedekindDomain C
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.Finite A C
inst✝⁴ : Module.Finite B C
inst✝³ : IsTorsionFree A C
inst✝² : IsTorsionFree B C
inst✝¹ : IsScalarTower A B C
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing C)
this✝³ : Algebra.IsSeparable (FractionRing B) (FractionRing C)
this✝² : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝¹ : FiniteDimensional (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing C)
this : FiniteDimensional (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ =
    (dual B (FractionRing B) 1)⁻¹ * ((extendedHom (FractionRing C) C) (dual A (FractionRing A) 1))⁻¹
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
⊢ minkowskiBound K 1 < MeasureTheory.volume (convexBodyLT K g)

Tactic:
rw [convexBodyLT_volume]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑(∏ w, g w ^ w.mult)
Module: Mathlib.RingTheory.Fintype

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

Tactic:
exact le_antisymm (fun a _ ↦ by simp [Subsingleton.elim a 0]) (Finset.subset_univ _)

Goal state after:
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
this : Nontrivial R
⊢ 3 ≤ #{-1} + 1 + 1

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
this : Nontrivial R
⊢ 1 ∉ {-1}

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
this : Nontrivial R
⊢ 0 ∉ {1, -1}

Tactic:
card_singleton

Goal state after:
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
this : Nontrivial R
⊢ 3 ≤ 1 + 1 + 1

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
this : Nontrivial R
⊢ 1 ∉ {-1}

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
this : Nontrivial R
⊢ 0 ∉ {1, -1}
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) * w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))⁻¹ < 1

Tactic:
map_inv₀,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) * (w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n)))⁻¹ < 1
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case h
a : ℕ
ha : Abundant 12
⊢ 2 * (a + 1) * 12 ∈ {n | Even n ∧ n.Abundant} ∧ a < 2 * (a + 1) * 12

Tactic:
grind [Abundant.mul_left ha (show 2 * (a + 1) ≠ 0 by grind)]

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
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = 1 * 1

Tactic:
quadraticCharFun_eq_one_of_char_two hF hab,

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
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ 1 = 1 * 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: 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
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨x, hx⟩ : ∃ x, Algebra.trace (A ⧸ p) (B ⧸ P) x ≠ 0 := by
    simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)

Goal state after:
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
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
x : B ⧸ P
hx : (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: 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
⊢ P * P ∣ P * a

Tactic:
exact mul_dvd_mul_left _ hPa

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

Goal state before:
pp: n : ℕ
Hn : n ≠ 0
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

Tactic:
rw [← Finset.nonempty_range_iff] at Hn

Goal state after:
n : ℕ
Hn : (Finset.range n).Nonempty
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case h
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)
⊢ ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * (λ ^ (3 * S.multiplicity - 5) * ↑S.u₅ * S.X ^ 3)

Tactic:
calc _ = λ^(3*(S.multiplicity-1))*S.u₅*S.X^3 := by ring
  _ = λ^2*λ^(3*S.multiplicity-5)*S.u₅*S.X^3 := by rw [this, pow_add]
  _ = λ^2*(λ^(3*S.multiplicity-5)*S.u₅*S.X^3) := by ring

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mpr
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 : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (algebraMap A B) (Ideal.under A P) = P * Q
⊢ ¬P ∣ differentIdeal A B

Tactic:
obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H

Goal state after:
case inr.mpr
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 : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (algebraMap A B) (Ideal.under A P) = P * Q
h₃ : Algebra.IsSeparable (Ideal.under A P).ResidueField P.ResidueField
h₄ :
  Ideal.map (algebraMap A (Localization.AtPrime P)) (Ideal.under A P) =
    IsLocalRing.maximalIdeal (Localization.AtPrime P)
⊢ ¬P ∣ differentIdeal A B
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)

Tactic:
Finset.sum_const,

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 : ι'
⊢ Finset.univ.card • ((⨆ ji, v (A ji)) * ⨆ i, v (x i)) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (Sum.elim x 0 i) = ⨆ i, v (x i)

pp: case inr.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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (Sum.elim x 0 i) = ⨆ i, ↑v (x i)

Tactic:
· exact H v

Goal state after:
case inr.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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
H : ∀ (v : AbsoluteValue K ℝ), ⨆ j, v (Sum.elim x 0 j) = ⨆ i, v (x i)
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (Sum.elim x 0 i) = ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

pp: case h₂
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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
· -- archimedean part: reduce to "local" statement `linearMap_apply_bound`
    rw [mul_assoc, ← prod_map_mul, ← prod_replicate, totalWeight, ← map_const', ← prod_map_mul]
    refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_
    rw [mul_comm (iSup _), ← mul_assoc]
    exact v.iSup_abv_linearMap_apply_le A x

Goal state after:
case h₂
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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (A i)) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case b0
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 0 ≤ (Multiset.map (fun i ↦ ↑(#s) * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod

Tactic:
exact prod_map_nonneg fun _ h ↦ by positivity

Goal state after:
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
⊢ (logHeight fun j ↦ (eval x) (p j)) ≤ log (max (mulHeightBound p) 1) + ↑N * logHeight x

Tactic:
simp_rw [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact (log_le_log <| by positivity) <| mulHeight_eval_le hp x

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := LinearMap.mulLeft (𝓞 K) ↑n
hf : Function.Injective ⇑↑f
⊢ span {↑n * ↑m} = Submodule.map f (span {↑m})

Tactic:
simp [LinearMap.map_span, f]

Goal state after:
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:
simp [mulHeight_eval_ge_aux p h]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ ({ toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) } %ₘ f).coeff ↑i = g i

Tactic:
(Polynomial.modByMonic_eq_self_iff h.monic).mpr,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff ↑i = g i

R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * (↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s)) = Φ j * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s))

Tactic:
simp only [cpow_neg, ← one_div, ofReal_div, ofReal_natCast, add_comm, add_div, ofReal_add,
      ofReal_mul, mul_div_cancel_left₀ (m : ℂ) (Nat.cast_ne_zero.mpr (NeZero.ne N))]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0

Tactic:
by
  rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
p : ℕ
hp : Nat.Prime p
k : ℕ
h : χ ↑p = 0
⊢ 0 ≤ ∑ x ∈ Finset.range (k + 1), χ ↑p ^ x

Tactic:
refine Finset.sum_nonneg fun i _ ↦ ?_
    simp only [h, le_refl, pow_nonneg]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))

Tactic:
have step2 :=
    has_pointwise_sum_fourier_series_of_summable
      ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ fourierCoeff (⇑B) i • (fourier i) ↑y) (B ↑y)
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ (fun w ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] fun x ↦ 1 / x

Tactic:
have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le

Goal state after:
N : ℕ
inst✝ : NeZero N
H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0) (𝓝 (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))
⊢ (fun w ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] fun x ↦ 1 / x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x ↦ ↑x

Tactic:
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).hasDerivAt

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * ↑y)) (1 + I * ↑y)
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x ↦ ↑x