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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ 1 / ‖h‖ * (1 / ‖𝕢 h (↑x + 1 / ↑n * I)‖ ^ n * ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))

Tactic:
Real.norm_of_nonneg hh.le,

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ 1 / h * (1 / ‖𝕢 h (↑x + 1 / ↑n * I)‖ ^ n * ‖f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }‖) ≤
    1 / h * (1 / Real.exp (-2 * Real.pi / h) * (C * ↑n ^ e))
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G : Type u_1
inst✝³ : Neg G
inst✝² : Preorder G
inst✝¹ : LocallyFiniteOrder G
inst✝ : atTop.NeBot
⊢ (symmetricIoo G).filter.NeBot

Tactic:
simp [symmetricIoo, Filter.NeBot.map]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ (symmetricIoo G).filter ≤ atTop

Tactic:
rw [symmetricIoo, map_le_iff_le_comap, ← @tendsto_iff_comap]
    exact tendsto_Ioo_neg_atTop_atTop

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

Goal state before:
pp: z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
        (2 * (↑π ^ 2 / 6) -
          8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n)))

Tactic:
mul_sub,

Goal state after:
z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ * (2 * (↑π ^ 2 / 6)) -
        (↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
          (8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n)))
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((F - G) ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z

Tactic:
rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
    deriv_sub hFz hGz, mul_sub]

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

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 / (↑z).sqrt + logDeriv η ↑z

Tactic:
div_eq_mul_inv,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + logDeriv η ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ ((fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) ∘ fun τ ↦ 𝕢 1 ↑τ) x ^ 24) atImInfty (𝓝 (1 ^ 24))
⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) atImInfty (𝓝 1)

Tactic:
simp only [Periodic.qParam, ofReal_one, div_one, comp_apply, one_pow, eta_q] at *

Goal state after:
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ (∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1))) ^ 24) atImInfty (𝓝 1)
⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑x) ^ (n + 1)) ^ 24) atImInfty (𝓝 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
a b : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [add_div]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
hk2 : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
induction k using Nat.strong_induction_on with | h k ihn =>
  have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind
  rcases this with hk | hk | hk
  · -- `k < 3`: direct case-by-case check
    interval_cases k
    · simpa using! levelOne_weight_zero_rank_one
    · grind
    · simpa [Nat.ModEq] using levelOne_weight_two_rank_zero
  · -- `3 ≤ k < 12`: rank decomposition + the weight `k - 12` space is zero
    rw [rank_eq_one_add_rank_cuspForm hk.1 hk2, CuspForm.discriminantEquiv.rank_eq,
      levelOne_neg_weight_rank_zero (by lia)]
    have : k ∈ (Finset.Icc 3 11).filter Even := by grind
    fin_cases this <;> simp [Nat.ModEq]
  · -- `12 ≤ k`: rank decomposition + induction hypothesis at weight `k - 12`
    rw [rank_eq_one_add_rank_cuspForm (by lia) hk2, CuspForm.discriminantEquiv.rank_eq,
      show ((k : ℤ) - 12 : ℤ) = ((k - 12 : ℕ) : ℤ) by lia,
      ihn (k - 12) (by lia) (by grind)]
    simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]
    split_ifs <;> grind

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
x : ℕ
⊢ ∑' (n : ℤ), ∑ m ∈ Ico (-↑x) ↑x, 1 / (↑n * ↑z + ↑m) ^ 2 = ∑ n ∈ Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

Tactic:
Summable.tsum_finsetSum

Goal state after:
z : ℍ
x : ℕ
⊢ ∑ i ∈ Ico (-↑x) ↑x, ∑' (b : ℤ), 1 / (↑b * ↑z + ↑i) ^ 2 = ∑ n ∈ Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

z : ℍ
x : ℕ
⊢ ∀ i ∈ Ico (-↑x) ↑x, Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (fun n ↦ rexp (-π * τ.im) * rexp (-π * τ.im) ^ n) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))

Tactic:
div_eq_mul_inv,

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)
⊢ HasSum (fun n ↦ rexp (-π * τ.im) * rexp (-π * τ.im) ^ n) (rexp (-π * τ.im) * (1 - rexp (-π * τ.im))⁻¹)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
⊢ IsCompact (truncatedFundamentalDomain y)

Tactic:
by
  rw [isEmbedding_coe.isCompact_iff, coe_truncatedFundamentalDomain,
    Metric.isCompact_iff_isClosed_bounded]
  constructor
  · -- show closed
    apply (isClosed_le continuous_const Complex.continuous_im).inter
    apply (isClosed_le Complex.continuous_im continuous_const).inter
    apply (isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const).inter
    exact isClosed_le continuous_const continuous_norm
  · -- show bounded
    refine (Metric.isBounded_iff_subset_closedBall 0).mpr ⟨√((1 / 2) ^ 2 + y ^ 2), fun z hz ↦ ?_⟩
    simp only [mem_closedBall_zero_iff]
    refine le_of_sq_le_sq ?_ (by positivity)
    rw [Real.sq_sqrt (by positivity), Complex.norm_eq_sqrt_sq_add_sq, Real.sq_sqrt (by positivity)]
    apply add_le_add
    · rw [sq_le_sq, abs_of_pos <| one_half_pos (α := ℝ)]
      exact hz.2.2.1
    · rw [sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)]
      exact hz.2.1

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g

Tactic:
exact ⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ↑p ^ 1 ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
rw [pow_one]
    exact dvd_geom_sum₂_self hxy

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) (x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

pp: case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

pp: case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k

Tactic:
emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx,

Goal state after:
case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) (x - y) + ↑(multiplicity p (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / (2 * ↑n / ↑(h Γ)) ^ s * (2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
have : (2 * n / h Γ : ℂ) ^ s = 2 ^ s * n ^ s / h Γ ^ s := by
      rw [← ofReal_ofNat, ← ofReal_natCast, ← ofReal_mul,
        div_cpow_ofReal_nonneg (by grind) Γ.strictWidthInfty_nonneg, ofReal_mul,
        mul_cpow_ofReal_nonneg zero_le_two n.cast_nonneg]

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / (2 * ↑n / ↑(h Γ)) ^ s * (2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
⊢ ∀ (x : Πʳ (i : ι), [R i, A i] × Y), ContinuousAt f x

Tactic:
ContinuousAt

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
⊢ ∀ (x : Πʳ (i : ι), [R i, A i] × Y), Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
⊢ ∀ (x : Y × Πʳ (i : ι), [R i, A i]), ContinuousAt f x

Tactic:
ContinuousAt

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
⊢ ∀ (x : Y × Πʳ (i : ι), [R i, A i]), Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
⊢ ∀ (x : (j : n) → Πʳ (i : ι), [A j i, C j i]), ContinuousAt f x

Tactic:
ContinuousAt

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
⊢ ∀ (x : (j : n) → Πʳ (i : ι), [A j i, C j i]), Tendsto f (𝓝 x) (𝓝 (f x))
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)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K).toAddSubgroup ⧸
        (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup)

Tactic:
rw [← AddSubgroup.index_ne_zero_iff_finite]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : polarSpace K) in (polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (x.1 ↑w)) * f (↑(polarSpaceCoord K).symm x) =
    ∫⁻ (x : mixedSpace K), f x

Tactic:
rw [← (volume_preserving_homeoRealMixedSpacePolarSpace K).setLIntegral_comp_preimage_emb
    (homeoRealMixedSpacePolarSpace K).measurableEmbedding,
    ← mixedEmbedding.lintegral_comp_polarCoord_symm, polarSpaceCoord_target,
    ← Homeomorph.image_eq_preimage_symm, Homeomorph.preimage_image,
    mixedEmbedding.polarCoord_target]
  simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_snd]

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)ˣ
⊢ IsMaxRank u ↔ (Subgroup.closure (Set.range u)).FiniteIndex

Tactic:
classical
  have h₁ : (closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
      Finite (unitLattice K ⧸ span ℤ (Set.range ((logEmbeddingEquiv K) ∘ Additive.toMul.symm ∘
        QuotientGroup.mk ∘ u))) := by
    change _ ↔ Finite ((unitLattice K).toAddSubgroup ⧸ (span ℤ (Set.range _)).toAddSubgroup)
    rw [← AddSubgroup.index_ne_zero_iff_finite]
    have := index_map (closure (Set.range u)) (QuotientGroup.mk' (torsion K))
    rw [QuotientGroup.ker_mk', QuotientGroup.range_mk', index_top, mul_one] at this
    rw [← this, ← index_toAddSubgroup, ← AddSubgroup.index_map_equiv
        _ (logEmbeddingEquiv K).toAddEquiv, Set.range_comp, ← LinearEquiv.coe_coe,
      ← map_span (logEmbeddingEquiv K).toLinearMap,
      map_toAddSubgroup, span_int_eq_addSubgroupClosure,
      MonoidHom.map_closure, toAddSubgroup_closure, Set.range_comp, Set.range_comp,
      QuotientGroup.coe_mk', ← Equiv.image_symm_eq_preimage]
    rfl
  have h₂ : DiscreteTopology
      (span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) := by
    rw [← SetLike.isDiscrete_iff_discreteTopology]
    refine (inferInstance : DiscreteTopology (unitLattice K)).isDiscrete.mono ?_
    rw [SetLike.coe_subset_coe, Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    exact ⟨Additive.ofMul (u i), mem_top, rfl⟩
  rw [finiteIndex_iff_sup_torsion_finiteIndex, finiteIndex_iff, h₁, finiteQuotient_iff,
    unitLattice_rank, ← Set.finrank, IsMaxRank, linearIndependent_iff_card_eq_finrank_span,
    Real.finrank_eq_int_finrank_of_discrete h₂, Set.finrank, Set.finrank, ← finrank_map_subtype_eq,
    map_span, ← Set.range_comp', eq_comm]
  simp

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 : mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x)) = 1
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      ((↑(↑x✝).mult)⁻¹ * x ↑x✝ -
        Real.log (mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x))) * (↑(finrank ℚ K))⁻¹) =
    x ↑x✝

Tactic:
mul_sub,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x)) = 1
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * ((↑(↑x✝).mult)⁻¹ * x ↑x✝) -
      ↑(↑x✝).mult * (Real.log (mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMap x))) * (↑(finrank ℚ K))⁻¹) =
    x ↑x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log (↑w x) - ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    ↑(↑w).mult * (Real.log (↑w x) - Real.log (mixedEmbedding.norm ((mixedEmbedding K) x)) * (↑(finrank ℚ K))⁻¹)

Tactic:
mul_sub,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log (↑w x) - ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    ↑(↑w).mult * Real.log (↑w x) -
      ↑(↑w).mult * (Real.log (mixedEmbedding.norm ((mixedEmbedding K) x)) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

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

Tactic:
by
  simp only [ZModXQuotSpanEquivQuotSpan, algebraMap_int_eq,
    RingEquiv.trans_apply, AlgEquiv.coe_ringEquiv, quotientEquivAlgOfEq_mk,
    quotientEquiv_symm_apply, quotientMap_mk, RingHom.coe_coe, mapEquiv_symm_apply,
    Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom]
  exact congr_arg (quotientEquivAlgOfEq ℤ (by simp [map_span])) <|
    quotMapEquivQuotQuotMap_symm_apply (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral Q

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}
⊢ span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}

Tactic:
rw [span_insert]

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
w : InfinitePlace K
hw : w ≠ w₀
⊢ ∑ x_1, x ↑x_1 • ↑((Finsupp.single (equivFinRank.symm x_1) 1) (equivFinRank.symm ⟨w, hw⟩)) ∈ Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
Finsupp.single_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ∑ x_1, x ↑x_1 • ↑(if equivFinRank.symm x_1 = equivFinRank.symm ⟨w, hw⟩ then 1 else 0) ∈ Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x, (↑x.mult)⁻¹ = 2⁻¹ ^ nrComplexPlaces K

Tactic:
simp [prod_eq_prod_mul_prod, mult_isReal, mult_isComplex]

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
⊢ HasFDerivAt (↑expMapBasis) (fderiv_expMapBasis K x) x

Tactic:
by
  change HasFDerivAt (expMap ∘ (completeBasis K).equivFunL.symm) (fderiv_expMapBasis K x) x
  exact (hasFDerivAt_expMap _).comp x (completeBasis K).equivFunL.symm.hasFDerivAt

Goal state after: