mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ 2⁻¹ * ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖

Tactic:
have : Finset.Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x} := by
    lift x to ℕ using by positivity
    convert! Finset.Icc_succ_succ (x - 1) (x - 1) <;> grind

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
⊢ ∏' (n : ℕ), (1 - eta_q n z) ≠ 0

Tactic:
refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_
  · exact fun i ↦ by simpa using! one_sub_eta_q_ne_zero i hz
  · simpa [eta_q, ← summable_norm_iff] using! summable_eta_q ⟨z, hz⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
n : ℕ
⊢ logDeriv (fun x ↦ 1 - eta_q n x) z = 2 * ↑π * I * (↑n + 1) * -eta_q n z / (1 - eta_q n z)

Tactic:
have h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (n + 1) * x)) =
      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (n + 1) * x) := by aesop
  simp_rw [eta_q_eq_cexp, h2, logDeriv_one_sub_mul_cexp_comp 1
    (g := fun x ↦ (2 * π * I * (n + 1) * x)) (by fun_prop), deriv_const_mul_id]
  simp

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
this :
  D (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z =
    (↑1)⁻¹ * (D F ∣[k + 2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z
⊢ D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ - fun z ↦
        ↑k * (2 * ↑π * I)⁻¹ *
            (↑(↑γ 1 0) /
              denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
          (F ∣[k] γ) z)
      z

Tactic:
simpa [ModularForm.SL_slash] using this

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) atImInfty (𝓝 1)

Tactic:
by
  have htprod : Tendsto (fun q : ℂ ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1) := by
    have := tendsto_tprod_one_add_of_dominated_convergence (𝓕 := 𝓝 0) (g := 0)
      (f := fun (q : ℂ) (n : ℕ) ↦ -q ^ (n + 1)) (bound := fun n ↦ (1 / 2 : ℝ) ^ (n + 1))
    simp only [Pi.zero_apply, norm_neg, norm_pow, add_zero, tprod_one] at this
    simp_rw [sub_eq_add_neg]
    refine this
      (by simpa only [pow_succ'] using (summable_geometric_of_abs_lt_one (by norm_num)).mul_left _)
      (fun k ↦ by simpa using ((continuous_pow (M := ℂ) (k + 1)).tendsto 0).neg) ?_
    filter_upwards [Metric.ball_mem_nhds (0 : ℂ) (by norm_num : (0 : ℝ) < 1 / 2)] with q hq k
    exact pow_le_pow_left₀ (norm_nonneg _) (mem_ball_zero_iff.mp hq).le _
  have := (htprod.comp (UpperHalfPlane.qParam_tendsto_atImInfty zero_lt_one)).pow 24
  simp only [Periodic.qParam, ofReal_one, div_one, comp_apply, one_pow, eta_q] at *
  convert! this using 2 with τ
  rw [Multipliable.tprod_pow]
  apply (multipliableLocallyUniformlyOn_eta.multipliable τ.2).congr
  simp [eta_q, Periodic.qParam, ← exp_nat_mul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 Δ) = 1

Tactic:
by
  have hmem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) 1 := Metric.mem_ball_self one_pos
  calc (qExpansion 1 Δ).coeff 1
      = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 := by
        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]
    _ = derivWithin (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 :=
        derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)
    _ = 1 := by
        simp [derivWithin_fun_mul differentiableWithinAt_fun_id
          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: 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 : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1)

Tactic:
rw [← neg_pow]

Goal state after:
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 : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-(2 * ↑π * I)) ^ (k + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))

Tactic:
G2_eq_tsum_symmetricIco,

Goal state after:
z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop
    (𝓝 ((↑z ^ 2)⁻¹ * ∑'[symmetricIco ℤ] (m : ℤ), e2Summand m (S • z)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
by
  rw [← (finTwoArrowEquiv ℤ).symm.tsum_eq, finTwoArrowEquiv_symm_apply,
    Summable.tsum_prod (summable_prod_eisSummand hk z),
    tsum_int_eq_zero_add_two_mul_tsum_pnat (fun n ↦ ?h₁)
      (by simpa using (summable_prod_eisSummand hk z).prod)]
  case h₁ =>
    nth_rewrite 1 [← tsum_comp_neg]
    exact tsum_congr fun y ↦ by simp [eisSummand, ← neg_add _ (y : ℂ), -neg_add_rev, hk2.neg_pow]
  have H (b : ℕ+) := qExpansion_identity_pnat (k := k - 1) (by grind) ⟨b * z, by simpa using z.2⟩
  simp_rw [show k - 1 + 1 = k by grind, one_div] at H
  simp only [neg_mul] at H
  rw [nsmul_eq_mul, mul_assoc]
  congr
  · simp [eisSummand, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (by grind) hk2]
  · suffices ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * (m * z)) ^ (n : ℕ) =
        ∑' (m : ℕ+) (n : ℕ+), (n : ℕ) ^ (k - 1) * cexp (2 * π * I * z) ^ (m * n : ℕ) by
      simp [eisSummand, H, tsum_mul_left,
        ← tsum_prod_pow_eq_tsum_sigma (k - 1) (norm_exp_two_pi_I_lt_one z), this]
    simp_rw [← Complex.exp_nat_mul]
    exact tsum_congr₂ (fun m n ↦ by push_cast; ring_nf)

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, y ^ i * x ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)

Tactic:
dvd_geom_sum₂_iff_of_dvd_sub

Goal state after:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ↑n * x ^ (n - 1) ↔ p ∣ ↑n * x ^ (n - 1)

R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : IsUnit x
⊢ (∀ (i : ι), IsUnit (x i)) ∧ ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩

Tactic:
by
  simp only [isUnit_iff_exists, RestrictedProduct.ext_iff, ← forall_and] at hx
  simp only [isUnit_iff_exists]
  choose b hb using hx
  exact ⟨Classical.skolem.symm.1 ⟨b, hb⟩, by filter_upwards [x.2, b.2] using
    fun i hx hb ↦ ⟨hx, ⟨b i, hb⟩, by simp_all [← SetLike.coe_eq_coe]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

Tactic:
by
  have : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3 := by
    refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_
    simp [← Nat.pow_two_sub_pow_two x 1]
    grind [Nat.eight_dvd_sq_sub_one_of_odd]
  have := pow_two_sub_one h1x hx hn hneven
  grind [← padicValNat.mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(polarSpaceCoord K).symm

Tactic:
rw [polarSpaceCoord, OpenPartialHomeomorph.transHomeomorph_symm_apply]
  exact (measurable_polarCoord_symm K).comp (Homeomorph.measurable _)

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

Goal state before:
pp: case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ (normAtPlace ↑w) x ≠ 0

Tactic:
exact mixedEmbedding.norm_ne_zero_iff.mp hx w

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = w x

Tactic:
norm_embedding_eq

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ w x = w x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑({
              toFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n) ab.1, ab.2),
              invFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n).symm ab.1,
                  ab.2),
              left_inv := ⋯, right_inv := ⋯ }
            ({ toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x ↦ ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯,
                right_inv := ⋯ }
              (((integerSetEquiv K).subtypeEquiv ⋯) a))).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
Equiv.subtypeEquiv_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑({
              toFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n) ab.1, ab.2),
              invFun := fun ab ↦
                ((Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal ↑I) fun I ↦ absNorm ↑I = n).symm ab.1,
                  ab.2),
              left_inv := ⋯, right_inv := ⋯ }
            ({ toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, (↑x).2), invFun := fun x ↦ ⟨(↑x.1, x.2), ⋯⟩, left_inv := ⋯,
                right_inv := ⋯ }
              ⟨(integerSetEquiv K) ↑a, ⋯⟩)).1 =
    Ideal.span {↑(preimageOfMemIntegerSet ↑a)}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
by
  obtain hs | hs := le_or_gt 0 s
  · simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]
    rw [torsionOrder, ← Nat.card_prod]
    refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _
      (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩)
      (fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_
    simp_rw [Subtype.mk.injEq]
    calc _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _} // absNorm I.1.1 = i} × torsion K :=
        Equiv.prodSubtypeFstEquivSubtypeProd
      _ ≃ {I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
        (p := fun I : (Ideal (𝓞 K))⁰ ↦ J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊)
        (q := fun I ↦ absNorm I.1 = i))
      _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by grind
      _ ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i} :=
            (idealSetEquivNorm K J i).symm
      _ ≃ {a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i} := by
        simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
        rfl
      _ ≃ {b : {a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊} //
            intNorm (idealSetEquiv K J b).1 = i} :=
        (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm
  · simp_rw [lt_iff_not_ge.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_ge.mp
      (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
      zero_mul]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsTotallyComplex K

Tactic:
have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝¹ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMap ((completeBasis K) w₀) ^ x w₀ * ↑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:
expMap_basis_of_eq,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun x ↦ Real.exp 1) ^ x w₀ * ↑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
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : Fin (rank K)
⊢ (logEmbedding K) (Additive.ofMul (fundSystem K x✝)) =
    (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) x✝

Tactic:
rw [logEmbedding_fundSystem, Basis.ofZLatticeBasis_apply]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(unitOfCoprime (p ^ f) ⋯) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = ↑1

Tactic:
coe_unitOfCoprime,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : root P ^ (p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = root P
⊢ ↑(p ^ f) ^ orderOf (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)) = ↑1
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) ∈
    normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))

Tactic:
· rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]
      exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
w : InfinitePlace K
hw : ¬w = w₀
⊢ ↑expMapBasis.symm x w ∈ Set.Ico 0 1

Tactic:
by simpa [hw] using h w

Goal state after:
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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ (span {⋯.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
ramificationIdx_span_zeta_sub_one

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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ p ^ k * (p - 1) = p ^ k * (p - 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
this : IsGalois ℚ K
⊢ (span {⋯.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)

Tactic:
ramificationIdx_span_zeta_sub_one

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
this : IsGalois ℚ K
⊢ p ^ k * (p - 1) = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ P.ramificationIdx ℤ = 1

Tactic:
ramificationIdx_eq_of_not_dvd p K P hm

Goal state after:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left✝ : P.IsPrime
right✝ : P.LiesOver 𝒑
⊢ 1 = 1
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ 0 ≤ dirichletDensity S

Tactic:
rw [dirichletDensity]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ 0 ≤ if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ dirichletDensity S ≤ 1

Tactic:
rw [dirichletDensity]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ (if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0) ≤ 1
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ dirichletDensity S ≤ 1

Tactic:
rw [dirichletDensity]
  split_ifs with h
  · exact h.choose_spec.le_one
  · exact zero_le_one

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f z = g z

Tactic:
← Rat.num_div_den z,

Goal state after:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f (↑z.num / ↑z.den) = g (↑z.num / ↑z.den)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : ‖A i j‖ < 1
⊢ A i j = 0

Tactic:
Int.norm_eq_abs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
i : α
j : β
h : |↑(A i j)| < 1
⊢ A i j = 0
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
a✝ : E
n : ℕ
x : ℤ_[p]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ ‖f‖ ≤
    ‖({ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          f).toBCF‖

Tactic:
← (hasSum_mahler f).tsum_eq

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
a✝ : E
n : ℕ
x : ℤ_[p]
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
f : C(ℤ_[p], E)
⊢ ‖∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f) 0) b‖ ≤
    ‖({ toFun := fun f ↦ { toFun := fun x ↦ Δ_[1]^[x] (⇑f) 0, continuous_toFun := ⋯, zero_at_infty' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ }
          (∑' (b : ℕ), mahlerTerm (Δ_[1]^[b] (⇑f) 0) b)).toBCF‖
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
⊢ ∀ (o : Set C(X × Y, R)), IsOpen o → f ∈ o → (o ∩ Set.range ⇑tensorHom).Nonempty

Tactic:
Set.nonempty_def

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
⊢ ∀ (o : Set C(X × Y, R)), IsOpen o → f ∈ o → ∃ x, x ∈ o ∩ Set.range ⇑tensorHom
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < a.x ^ 2
h2 : 0 < a.y ^ 2
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Tactic:
nlinarith

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a = 1 ∨ a = -1

Tactic:
rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop

Goal state after:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1