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

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ∀ ⦃x : L⦄, (∀ (a : L), (Algebra.trace K L) (x * a) ∈ (algebraMap A K).range) → x = 0

Tactic:
RingHom.mem_range

Goal state after:
case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ∀ ⦃x : L⦄, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) → x = 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case pos.zero
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ (0 + 1))
hC : IsCyclotomicExtension {q ^ (0 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (0 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Goal state after:
case pos.zero
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this✝ : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
q : ℕ
hn : 2 < 2
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ (0 + 1))
hC : IsCyclotomicExtension {q ^ (0 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (0 + 1) = n
⊢ ↑p ∣ ↑q ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I J : FractionalIdeal B⁰ L
⊢ dual A K 1 ≠ 0

Tactic:
simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]

Goal state after:
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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ 1 / traceDual A (FractionRing A) 1 ≤ (Algebra.linearMap B (FractionRing B)).range

Tactic:
have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A)
    (1 : FractionalIdeal B⁰ (FractionRing B))

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✝⁵ : IsIntegrallyClosed A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Algebra.IsIntegral A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : (FractionalIdeal.dual A (FractionRing A) 1)⁻¹ ≤ 1
⊢ 1 / traceDual A (FractionRing A) 1 ≤ (Algebra.linearMap B (FractionRing B)).range
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)
⊢ differentIdeal A C = differentIdeal B C * Ideal.map (algebraMap B C) (differentIdeal A B)

Tactic:
by
  have : Algebra.IsSeparable (FractionRing B) (FractionRing C) :=
    isSeparable_tower_top_of_isSeparable (FractionRing A) _ _
  have : Algebra.IsSeparable (FractionRing A) (FractionRing B) :=
    isSeparable_tower_bot_of_isSeparable _ _ (FractionRing C)
  have : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
  have : FiniteDimensional (FractionRing A) (FractionRing C) := .of_isLocalization A C A⁰
  have : FiniteDimensional (FractionRing B) (FractionRing C) := .of_isLocalization B C B⁰
  rw [← coeIdeal_inj (K := FractionRing C), coeIdeal_mul, coeIdeal_differentIdeal A
    (FractionRing A), coeIdeal_differentIdeal B (FractionRing B)]
  rw [← extendedHom_coeIdeal_eq_map (K := FractionRing B), coeIdeal_differentIdeal A
    (FractionRing A), map_inv₀, ← mul_inv, ← inv_eq_iff_eq_inv, inv_inv]
  exact dual_eq_dual_mul_dual A (FractionRing A) (FractionRing B) B C (FractionRing C)

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsDedekindDomain B
inst✝ : IsTorsionFree A B
x : B
hx : K[(algebraMap B L) x] = ⊤
⊢ (aeval x) (derivative (minpoly A x)) ∈ differentIdeal A B

Tactic:
by
  refine SetLike.le_def.mp ?_ (Ideal.mem_span_singleton_self _)
  rw [← conductor_mul_differentIdeal A K L x hx]
  exact Ideal.mul_le_right

Goal state after:
Module: Mathlib.RingTheory.Fintype

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

Tactic:
rcases lt_or_eq_of_le h with h | h

Goal state after:
case inl
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}

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}
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₀ }
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
let v := fun w : { w : InfinitePlace K // w ≠ w₀ } ↦
    logEmbedding K (Additive.ofMul (exists_unit K w).choose)

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)
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom)
        (Additive.toMul a₁✝)) =
    Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯).toMonoidHom)
        (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝

Tactic:
MulEquiv.coe_toMonoidHom,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a₁✝ a₂✝ : Additive ((𝓞 K)ˣ ⧸ torsion K)
h :
  Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯))
        (Additive.toMul a₁✝)) =
    Multiplicative.toAdd
      ((⇑(QuotientGroup.kerLift (AddMonoidHom.toMultiplicativeRight (logEmbedding K))) ∘
          ⇑(QuotientGroup.quotientMulEquivOfEq ⋯))
        (Additive.toMul a₂✝))
⊢ a₁✝ = a₂✝
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
ha : a ≠ 0
⊢ quadraticCharFun F a = 1

Tactic:
by
  simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]
  exact fun h ↦ (h (FiniteField.isSquare_of_char_two hF a)).elim

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
a : F
ha : a ≠ 0
⊢ (quadraticChar F) a ^ 2 = 1

Tactic:
rwa [pow_two, ← map_mul, ← pow_two, quadraticChar_sq_one']

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

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : ¬a = 0
⊢ (quadraticChar F) a = -1 ↔ ¬IsSquare a

Tactic:
rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]

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
x✝ : ∃ a, (quadraticChar F) a = -1
a : F
ha : ¬IsUnit a
⊢ ¬(quadraticChar F) a = -1

Tactic:
exact ne_of_eq_of_ne ((quadraticChar F).map_nonunit ha) (mt zero_eq_neg.mp one_ne_zero)

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
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = (quadraticChar F) a + 1

Tactic:
(quadraticChar_one_iff_isSquare h₀).mpr h

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = 1 + 1
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✝ ∈ insert b (insert (-b) ∅)

Tactic:
insert_empty_eq,

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, -b}
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7

Tactic:
FiniteField.isSquare_two_iff,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ Fintype.card (ZMod p) % 8 ≠ 3 ∧ Fintype.card (ZMod p) % 8 ≠ 5 ↔ p % 8 = 1 ∨ p % 8 = 7
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ generator (Ideal.span (Nat.cast '' s)) = 0 ↔ s ⊆ {0}

Tactic:
← eq_bot_iff_generator_eq_zero,

Goal state after:
s : Set ℕ
⊢ Ideal.span (Nat.cast '' s) = ⊥ ↔ s ⊆ {0}
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inl
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)
inst✝ : ⊥.IsPrime
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization B⁰ (Localization.AtPrime ⊥)
this : FormallyUnramified K L
⊢ FormallyUnramified A L

Tactic:
refine .comp A K L

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case h
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)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₆ : 2 * p ∣ A * B - 1
this : A * B * (b ^ 2 - 1) = (b ^ (2 * p) - 1) / (b ^ 2 - 1) * (b ^ 2 - 1)
⊢ b ^ (2 * p) - 1 = A * B * (b ^ 2 - 1)

Tactic:
simpa only [add_comm, Nat.div_mul_cancel hd, Nat.sub_add_cancel hi_bpowtwop] using this.symm

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ (1 * ↑η ^ 2 - 1 * 1) * gcd S.a S.b
⊢ p ∣ λ

Tactic:
rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime, ← dvd_neg] at this

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ -(↑η ^ 2 - 1)
⊢ p ∣ λ
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

Tactic:
rw [Finset.sum_insert ha]
    grw [hv .., ih]
    refine max_le ?_ ?_
    · exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl
    · 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.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight (Sum.elim x 0) = mulHeight x

Tactic:
have hx' : Sum.elim x (0 : ι' → K) ≠ 0 := ne_iff.mpr ⟨.inl i, by simpa using hi⟩

Goal state after:
case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
⊢ mulHeight (Sum.elim x 0) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
nth_rewrite 1 [show n = -n.natAbs by grind]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ (-↑n.natAbs)) = mulHeight₁ x ^ n.natAbs
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * termTSum s

Tactic:
rw [termTSum_of_lt hs]
  generalize (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) = Z
  field [(show s - 1 ≠ 0 by linarith)]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x + -y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ (-y)

Tactic:
exact logHeight₁_add_le x (-y)

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

Goal state before:
pp: aux2 : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - termTSum 1))
this : termTSum 1 + γ = 1
⊢ Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
← eq_sub_iff_add_eq'

Goal state after:
aux2 : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - termTSum 1))
this : γ = 1 - termTSum 1
⊢ Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ s - 1 ≠ 0

Tactic:
· rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs

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

Goal state before:
pp: ⊢ (↑γ - log (4 * ↑π)) / 2 = ↑((γ - Real.log (4 * π)) / 2)

Tactic:
ofReal_div,

Goal state after:
⊢ (↑γ - log (4 * ↑π)) / 2 = ↑(γ - Real.log (4 * π)) / ↑2
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3.refine_2
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑q.den ≤ ⨆ i, |![q.num, ↑q.den] i|

pp: case e'_3.refine_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin 2
⊢ |![q.num, ↑q.den] i| ≤ max |q.num| ↑q.den

Tactic:
· exact Finite.le_ciSup_of_le 1 <| by simp

Goal state after:
case e'_3.refine_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin 2
⊢ |![q.num, ↑q.den] i| ≤ max |q.num| ↑q.den
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ = Pi.single n 1 i

pp: case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ 0 = Pi.single n 1 i

Tactic:
· calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]

Goal state after:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : ¬i < f.natDegree
⊢ 0 = Pi.single n 1 i
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case base
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
n : ℕ
hn₂ : Nat.succ 0 < orderOf χ
⊢ gaussSum χ ψ ^ Nat.succ 0 = gaussSum (χ ^ Nat.succ 0) ψ * ∏ j ∈ Ico 1 (Nat.succ 0), jacobiSum χ (χ ^ j)

Tactic:
| base =>

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
rw [toAddCircle_apply, ← (hasSum_expZeta_of_one_lt_re (j.val / N) hs).tsum_eq,
    LFunction_eq_LSeries _ hs, LSeries]

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), LSeries.term (fun x ↦ 𝕖 (j * ↑x)) s n = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 𝕖 (j * ↑n) / ↑n ^ s = cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑n) / ↑n ^ s

Tactic:
ofReal_div,

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 𝕖 (j * ↑n) / ↑n ^ s = cexp (2 * ↑π * I * (↑↑j.val / ↑↑N) * ↑n) / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 𝕖 (j * ↑n) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Tactic:
stdAddChar_apply

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rcases eq_or_ne N 1 with rfl | hN
  · simp [completedLFunction_modOne_eq, completedRiemannZeta_one_sub, rootNumber_modOne]
  -- facts about `χ` as function
  have h_sum : ∑ j, χ j = 0 := by
    refine χ.sum_eq_zero_of_ne_one (fun h ↦ hN.symm ?_)
    rwa [IsPrimitive, h, conductor_one] at hχ
  let ε := I ^ (if χ.Even then 0 else 1)
  -- gather up powers of N
  rw [rootNumber, ← mul_comm_div, ← mul_comm_div, ← cpow_sub _ _ (NeZero.ne _), sub_sub, add_halves]
  calc completedLFunction χ (1 - s)
  _ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s := by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
  _ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s := by
    congr 2 with j
    rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) := by
    rw [completedLFunction, completedLFunction_const_mul]
    ring
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
    rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ bernoulliFourierCoeff (k + 1) n = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
rw [bernoulliFourierCoeff_recurrence (k + 1) hn, if_neg (by grind), Nat.add_sub_cancel k 1, h'k,
      Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add]

Goal state after:
case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ 1 / (-2 * ↑π * I * ↑n) * -(↑(k + 1) * (-↑k ! / (2 * ↑π * I * ↑n) ^ k)) =
    -(↑(k + 1) * ↑k !) / ((2 * ↑π * I * ↑n) ^ k * (2 * ↑π * I * ↑n) ^ 1)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ riemannZeta s * LSeries (fun x ↦ B.χ ↑x) s = LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s