mathlib-initiative/mathlib-tactics huggingface dataset:
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 : FractionalIdeal B⁰ L
⊢ dual A K I = dual A K 1 * I⁻¹

Tactic:
by
  by_cases hI : I = 0; · simp [hI]
  apply le_antisymm
  · rw [le_mul_inv_iff₀ (pos_iff_ne_zero.2 hI), ← le_dual_iff A K hI]
  rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel₀ hI, mul_one]

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

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (NumberField.discr ↥F₁).natAbs.Coprime (NumberField.discr ↥F₂).natAbs

Tactic:
natAbs_discr n₁ F₁,

Goal state after:
K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime (NumberField.discr ↥F₂).natAbs
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ ↑⋯.unit ∈ torsion K

Tactic:
refine (CommGroup.mem_torsion _).mpr ⟨n, NeZero.pos n, ?_⟩

Goal state after:
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : NeZero n
ζ : K
hζ✝ : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot ⋯.unit n
⊢ Function.IsPeriodicPt (fun x ↦ ↑⋯.unit * x) n 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos
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₀.mult‖ * ‖Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))‖ ≤ ∑ i, ‖(logEmbedding K) (Additive.ofMul x) i‖
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

Tactic:
norm_neg,

Goal state after:
case pos
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₀.mult‖ * ‖Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))‖ ≤ ∑ i, ‖(logEmbedding K) (Additive.ofMul x) i‖
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ ((fun x ↦ (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}).Finite

Tactic:
refine (Embeddings.finite_of_norm_le K ℂ
        (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)} ⊆
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
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
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), w ↑y < ↑(g w)
⊢ ↑|(Algebra.norm ℚ) ↑y| ≤ ↑↑B

Tactic:
Rat.cast_natCast

Goal state after:
case refine_1
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
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), w ↑y < ↑(g w)
⊢ ↑|(Algebra.norm ℚ) ↑y| ≤ ↑B
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih : n < m → w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))
h : n < m + 1
hr : n = m
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB (m + 1))) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
| inl hr =>

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑u - ↑n = λ ^ 2 * x
⊢ ↑u - ↑n = 3 * (-↑η * x)

Tactic:
by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]

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

Goal state before:
pp: case neg.inr
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
hb' : b ^ (Fintype.card F / 2) = -1
⊢ (if a ^ (Fintype.card F / 2) * b ^ (Fintype.card F / 2) = 1 then 1 else -1) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
· have h := Ring.neg_one_ne_one_of_char_ne_two hF
      -- `-1 ≠ 1`
      simp only [hb', mul_neg, mul_one, h, if_false]
      rcases FiniteField.pow_dichotomy hF ha with ha' | ha' <;>
        simp only [ha', h, neg_neg, if_true, if_false]

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ˣ
ha : (quadraticChar F) ↑a = -1
hχ : quadraticChar F = 1
⊢ False

Tactic:
simp only [hχ, one_apply a.isUnit, reduceCtorEq] at ha

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ ∀ (q : ℕ), Prime q → q ∣ 2 ^ 2 ^ n + 1 - 1 → 3 ^ ((2 ^ 2 ^ n + 1 - 1) / q) ≠ 1

Tactic:
intro p

Goal state after:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
⊢ Prime p → p ∣ 2 ^ 2 ^ n + 1 - 1 → 3 ^ ((2 ^ 2 ^ n + 1 - 1) / p) ≠ 1
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
⊢ ℤ ∙ generator (Ideal.span (Nat.cast '' s)) = Ideal.span (Nat.cast '' s)

Tactic:
span_singleton_generator

Goal state after:
s : Set ℕ
⊢ Ideal.span (Nat.cast '' s) = Ideal.span (Nat.cast '' s)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h0 : setGcd s = 0
x✝¹ : ℕ
x✝ : x✝¹ ≥ 0
dvd : setGcd s ∣ x✝¹
⊢ x✝¹ ∈ span ↑∅

Tactic:
by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _

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

Goal state before:
pp: case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑↑x)⁻¹ ≤ 1 + Real.log ↑n

Tactic:
Rat.cast_natCast

Goal state after:
case neg
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∑ x ∈ Finset.Icc 1 n, (↑x)⁻¹ ≤ 1 + Real.log ↑n
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
hpaηb : p ∣ S.a + ↑η * S.b
hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b
⊢ Associated p λ

Tactic:
suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
  rw [← one_mul S.a] at hpaηb
  rw [← one_mul S.a] at hpaηsqb
  have := dvd_mul_sub_mul_mul_gcd_of_dvd hpaηb hpaηsqb
  rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this
  convert! (dvd_mul_of_dvd_left (dvd_mul_of_dvd_left this η) η) using 1
  symm
  calc _ = (-η.1 - 1 - η) * (-η - 1) := by rw [eta_sq, mul_assoc, ← pow_two, eta_sq]
  _ = 2 * η.1 ^ 2 + 3 * η + 1 := by ring
  _ = λ := by rw [eta_sq, coe_eta]; ring

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

Goal state before:
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.val

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
⊢ (vecCons 0 x ∘ ⇑e) j = Sum.elim x 0 j

Tactic:
match j with
    | .inl _ => simp [e]
    | .inr ⟨i, h⟩ =>
      simp [show i = 0 by lia, e, show Fin.castAdd n 0 = 0 from Fin.castAdd_mk _ _ zero_lt_one]

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

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

Tactic:
apply HasSum.tsum_eq

Goal state after:
s : ℝ
hs : 1 < s
⊢ HasSum (fun b ↦ term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)

Goal state after:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume ≤
    ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (1 + 1) ∂volume
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} ≠ ⊥
⊢ (∏ᶠ (x_1 : FinitePlace K),
        ↑(absNorm (x_1.maximalIdeal.asIdeal ^ multiplicity x_1.maximalIdeal.asIdeal (⨆ i, span {x i})))) *
      ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) =
    1

Tactic:
← finprod_mul_distrib ?hf <| .iSup (FinitePlace.hasFiniteMulSupport <| mod_cast hx ·)

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} ≠ ⊥
⊢ ∏ᶠ (i : FinitePlace K),
      ↑(absNorm (i.maximalIdeal.asIdeal ^ multiplicity i.maximalIdeal.asIdeal (⨆ i, span {x i}))) * ⨆ i_1, i ↑(x i_1) =
    1

case hf
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} ≠ ⊥
⊢ Function.HasFiniteMulSupport fun x_1 ↦
    ↑(absNorm (x_1.maximalIdeal.asIdeal ^ multiplicity x_1.maximalIdeal.asIdeal (⨆ i, span {x i})))
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})))⁻¹ = ⨆ i, v ↑(x i)

Tactic:
map_iInf_of_monotone _ Nat.mono_cast,

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, ↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)
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 : y ∈ univ \ {-1}
⊢ y / (1 + y) / (1 - y / (1 + y)) = y

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at hy

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 : ¬y = -1
⊢ y / (1 + y) / (1 - y / (1 + y)) = y
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

Tactic:
mulHeight_zero,

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

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

Tactic:
mulHeight_zero,

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ s - 1 ≠ 0

Tactic:
exact this

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
by
  have H : deriv (LFunctionTrivChar₁ n) s =
      deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s := by
    refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq
    exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_ofPred.mp hw) ..⟩
  rw [H, deriv_fun_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const,
    deriv_id'', one_mul, add_comm]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
have mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
      normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) := by
    simp [normalizedFactors_irreducible hf]
  suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
  rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
  use ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩ :
      Ideal S)
  rw [Multiset.map_eq_singleton]
  use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩
  refine ⟨?_, rfl⟩
  apply Multiset.map_injective Subtype.coe_injective
  rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
  exact normalizedFactors_irreducible hf

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5.h
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 ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a‖ * ‖z ^ 2‖ < 1

Tactic:
norm_pow,

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
⊢ ‖↑a‖ * ‖z‖ ^ 2 < 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - (‖z ^ n‖ ^ 2 - (z ^ n).re ^ 2))

Tactic:
norm_pow,

Goal state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((‖z‖ ^ n) ^ 2 - (z ^ n).re ^ 2))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : m ≤ n + 1
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

Tactic:
simp [hm, hF₀ _ hm]

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

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F₀ ∘ Subtype.val)

Tactic:
hFF'

Goal state after:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F' ∘ ⇑prodNatEquiv.symm)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ (-s).re ≤ 0

Tactic:
exact neg_re _ ▸ neg_nonpos.mpr <| hr.trans hs.le

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ AddChar F ℂ

Tactic:
letI ch := primitiveChar F ℂ <| by exact ringChar_ne F

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
ch : PrimitiveAddChar F ℂ := primitiveChar F ℂ ⋯
⊢ AddChar F ℂ
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ 1 < min (1 + (↑q.totient)⁻¹ / (C + C') / 2) 2

Tactic:
simpa only [lt_inf_iff, lt_add_iff_pos_right, Nat.ofNat_pos, div_pos_iff_of_pos_right,
          Nat.one_lt_ofNat, and_true] using div_pos hq h₀

Goal state after: