mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)

Tactic:
rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
m : ℤ
⊢ HasSum (fun b ↦ 1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1)) 0 (symmetricIco ℤ)

Tactic:
simp_rw [hasSum_symmetricIco_int_iff, telescope_aux z m]

Goal state after:
z : ℍ
m : ℤ
⊢ Tendsto (fun N ↦ 1 / (↑m * ↑z - ↑N) - 1 / (↑m * ↑z + ↑N)) atTop (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑n) atTop (𝓝 0)

Tactic:
by
  have := tendsto_zero_geometric_tsum_pnat (norm_exp_two_pi_I_lt_one ⟨_, im_pnat_div_pos 1 z⟩)
  simp only [← exp_nsmul, nsmul_eq_mul, Nat.cast_mul] at *
  exact this.congr <| by grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ↑g 1 0 = 0

Tactic:
rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl

Goal state after:
case inl
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : 1 • z ∈ 𝒟ᵒ
⊢ ↑1 1 0 = 0

case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ ↑(-1) 1 0 = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z

Tactic:
rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl

Goal state after:
case inl
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : 1 • z ∈ 𝒟ᵒ
⊢ z = 1 • z

case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ z = -1 • z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case inl
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : ↑(gammaSet 1 0 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(0, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(0, c).2) z

pp: case inr
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
hb : b ≠ 0
⊢ ∑' (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
· simp [show ((0 : ℂ) ^ k)⁻¹ = 0 by aesop, eisSummand_of_gammaSet_eq_divIntMap]

Goal state after:
case inr
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
hb : b ≠ 0
⊢ ∑' (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ UpperHalfPlane.coe '' 𝒟 = {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
ext x
  refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_le_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
  rintro ⟨τ, hτ, rfl⟩
  exact ⟨τ.im_pos, one_le_normSq_iff.mp hτ.1, hτ.2⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
z : ℂ
hz : 0 < z.im
h : { coe := z, coe_im_pos := hz } ∈ truncatedFundamentalDomain y
⊢ 1 ≤ ‖↑{ coe := z, coe_im_pos := hz }‖

Tactic:
simpa [Complex.normSq_eq_norm_sq] using h.1.1

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ regOfFamily u = |(of fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|

Tactic:
rw [regOfFamily_eq_zero hu, det_eq_zero_of_not_linearIndependent_rows, abs_zero]
    rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        ∏ x, ENNReal.ofReal (2 * π) ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
Finset.prod_const,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        ENNReal.ofReal (2 * π) ^ Finset.univ.card ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, (∃ x' ∈ ↑J, (algebraMap (𝓞 K) K) x' = a) ∧ (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
exists_exists_and_eq_and

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∑ j, of (fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))) i✝ j = 0

Tactic:
of_apply,

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
i✝ : Fin (rank K)
⊢ ∑ j, ↑(f j).mult * Real.log ((f j) ((algebraMap (𝓞 K) K) ↑(u i✝))) = 0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ rank K = |∏ w, 2|

Tactic:
Finset.prod_const,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ rank K = |2 ^ Finset.univ.card|
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ x,
          of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            w' x| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|

Tactic:
of_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ x, if h : True then ↑x.mult else ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨w', ⋯⟩))))| *
      |((of fun i w ↦
                if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).submatrix
            (fun x ↦ f ((f.symm w').succAbove x)) fun x ↦ f ((f.symm w').succAbove x)).det|
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ of (fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e i))))) (g.symm i) (g.symm j) =
    of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
      (f ((f.symm w').succAbove i)) (f ((f.symm w').succAbove j))

Tactic:
of_apply,

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(u (e (g.symm i))))) =
    of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
      (f ((f.symm w').succAbove i)) (f ((f.symm w').succAbove j))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(u (e (g.symm i))))) =
    of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
      (f ((f.symm w').succAbove i)) (f ((f.symm w').succAbove j))

Tactic:
of_apply,

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(u (e (g.symm i))))) =
    if h : f ((f.symm w').succAbove i) = w' then ↑(f ((f.symm w').succAbove j)).mult
    else
      ↑(f ((f.symm w').succAbove j)).mult *
        Real.log ((f ((f.symm w').succAbove j)) ((algebraMap (𝓞 K) K) ↑(u (e ⟨f ((f.symm w').succAbove i), h⟩))))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap (∑ i, x i • (completeBasis K) i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
Fintype.sum_eq_add_sum_subtype_ne _ w₀,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap (x w₀ • (completeBasis K) w₀ + ∑ i, x ↑i • (completeBasis K) ↑i) =
    Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst✝ : IsCyclotomicExtension S ℚ K
⊢ IsCMField K

Tactic:
by
  have : Algebra.IsIntegral ℚ K := integral S ℚ K
  obtain ⟨n, hn₁, hn₂⟩ := hS
  have : NeZero n := ⟨by positivity⟩
  obtain ⟨ζ, hζ⟩ := exists_isPrimitiveRoot ℚ K hn₁ (by grind)
  have : IsTotallyComplex K := by
    have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
    have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
    exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ K
  have := isAbelianGalois S ℚ K
  exact IsCMField.of_isAbelianGalois K

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
h_eq₁ :
  span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}
h_eq₂ : span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}
⊢ Ideal.map (Ideal.Quotient.mk (span {↑p})) (span {(aeval θ) Q}) =
    Ideal.map (↑(ZModXQuotSpanEquivQuotSpan hp))
      (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))

Tactic:
simp [map_span, ZModXQuotSpanEquivQuotSpan_mk_apply]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (b : InfinitePlace K),
    f.symm b ≠ f.symm w' →
      ∑ i,
          of (fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            (f.symm.symm (f.symm b)) (f.symm.symm (f.symm i)) =
        0

Tactic:
of_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (b : InfinitePlace K),
    f.symm b ≠ f.symm w' →
      (∑ i,
          if h : f.symm.symm (f.symm b) = w' then ↑(f.symm.symm (f.symm i)).mult
          else
            ↑(f.symm.symm (f.symm i)).mult *
              Real.log ((f.symm.symm (f.symm i)) ((algebraMap (𝓞 K) K) ↑(u (e ⟨f.symm.symm (f.symm b), h⟩))))) =
        0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
          (∑ i, (if i = w₀ then 0 else x i) • (completeBasis K) i) ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
Fintype.sum_eq_add_sum_subtype_ne _ w₀,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
          ((if w₀ = w₀ then 0 else x w₀) • (completeBasis K) w₀ +
              ∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i)
            ↑w)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (span {hζ.toInteger - 1}).LiesOver 𝒑

Tactic:
rw [liesOver_iff]

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ 𝒑 = under ℤ (span {hζ.toInteger - 1})
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ ∏ σ, span {hζ.toInteger - 1} = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
Finset.prod_const,

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
⊢ span {hζ.toInteger - 1} ^ Finset.univ.card = span {hζ.toInteger - 1} ^ Module.finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w

Tactic:
simpa [h, eq_comm] using hy w₀

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ), ↑(padicNorm p (x * y)) = ↑(padicNorm p x) * ↑(padicNorm p y)

Tactic:
simp only [padicNorm.mul, Rat.cast_mul, forall_const]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
⊢ False

Tactic:
obtain ⟨ha₀, hb₀⟩ := mul_ne_zero_iff.mp (by omega : a * b ≠ 0)

Goal state after:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ False
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * max 1 ‖A‖ * ↑B + 1

Tactic:
simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ + ∑ x, ↑B * ↑(A i x)⁻ ≤ ↑n * max 1 ‖A‖ * ↑B
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p m : ℕ
hpm : ¬p ∣ m
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hm : f ↑m < 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
bezout : a * ↑(p ^ k) + b * ↑(m ^ k) = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f ↑(a * ↑(p ^ k) + b * ↑(m ^ k))

Tactic:
bezout

Goal state after:
f : AbsoluteValue ℚ ℝ
p m : ℕ
hpm : ¬p ∣ m
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hm : f ↑m < 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
bezout : a * ↑(p ^ k) + b * ↑(m ^ k) = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f ↑1
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Tactic:
exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

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

Goal state before:
pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * ↑(finrank ℚ K) * c₂ K * A) ^ (↑p / (↑q - ↑p))

Tactic:
mul_assoc (q * _ : ℝ)

Goal state after:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ↑(finrank ℚ K) * supOfBasis K * (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * (max 1 (c K) * supOfBasis K) * (↑q * ↑(finrank ℚ K) * (c₂ K * A)) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
⊢ ∃ n, ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖

Tactic:
by
    obtain ⟨δ, hδp, hδ⟩ := Metric.continuousAt_iff.mp hf _ (norm_pos_iff.mpr hC)
    obtain ⟨n, hn'⟩ := PadicInt.denseRange_natCast.exists_dist_lt x hδp
    simpa only [← dist_eq_norm_sub'] using ⟨n, (hδ (dist_comm x n ▸ hn')).le⟩

Goal state after: