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

Goal state before:
pp: case mpr
a : SL(2, ℤ)
⊢ IsCusp (OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)) (mapGL ℝ).range

Tactic:
refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩

Goal state after:
case mpr.refine_1
a : SL(2, ℤ)
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic

case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map Rat.cast ((mapGL ℚ) a • ∞) =
    OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ f z * denom γ ↑z ^ k = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
denom,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ f z * (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range ↔ ∃ g, c = (mapGL ℝ) g • ∞

Tactic:
rw [isCusp_SL2Z_iff]
  constructor
  · rintro ⟨c, rfl⟩
    obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ
    refine ⟨g, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
      ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]
  · rintro ⟨g, rfl⟩
    refine ⟨mapGL ℚ g • ∞, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ (DirectSum.of (ModularForm Γ) k) f ^ n = (DirectSum.of (ModularForm Γ) (↑n * k)) (f.pow n)

Tactic:
grind [DirectSum.ofPow, DirectSum.of_eq_of_gradedMonoid_eq (gnpow_eq_pow f n)]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
⊢ Continuous fun τ ↦ τ.im ^ t

Tactic:
exact continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero

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

Goal state before:
pp: case h.left
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x ∈ gammaSet 1 r 0

Tactic:
mem_gammaSet_one,

Goal state after:
case h.left
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : IsCoprime (x 0) (x 1)
⊢ ↑r * x ∈ gammaSet 1 r 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableAt ℂ (⇑(eisensteinSeriesSIF a k) ∘ ↑ofComplex) ↑τ

Tactic:
refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)

Goal state after:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableOn ℂ (⇑(eisensteinSeriesSIF a k) ∘ ↑ofComplex) upperHalfPlaneSet
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd : 0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
· specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_
    · simpa using (not_le.mp hd).le
    convert! this using 2 <;> simp [neg_eq_iff_eq_neg, or_comm]

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd : 0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
by
  wlog hd : 0 ≤ g 1 1
  · specialize this hz (g := -g) (SL_neg_smul g z ▸ hg) (by simpa using hc) ?_
    · simpa using (not_le.mp hd).le
    convert! this using 2 <;> simp [neg_eq_iff_eq_neg, or_comm]
  have hd' : g 1 1 = 1 ∨ g 1 1 = -1 := by
    simpa [hc, isCoprime_zero_left, Int.isUnit_iff] using bottom_row_coprime g
  replace hd : g 1 1 = 1 := by grind
  have ha : g 0 0 = 1 := by grind [det_fin_two, g.property]
  let b := g 0 1
  have hgz : g = T ^ b := by
    ext i j
    rw [coe_T_zpow]
    fin_cases i <;> fin_cases j <;> tauto
  have hre : (g • z).re = b + z.re := by
    rw [hgz, ← coe_re, coe_T_zpow_smul_eq, add_re, coe_re, intCast_re, add_comm]
  have := (abs_sub_abs_le_abs_add ..).trans (hre ▸ hg.2)
  grw [sub_le_iff_le_add, hz.2, add_halves, ← Int.cast_abs, ← Int.cast_one, Int.cast_le,
    Int.abs_le_one_iff] at this
  rcases this with hb | hb | hb <;> rw [hb] at hgz
  · rw [hgz]
    simp
  · left
    rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_one] at hre
    linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]
  · right
    left
    rw [hgz, zpow_neg_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_neg, Int.cast_one] at hre
    linarith [(le_abs_self _).trans hz.2, (le_abs_self _).trans (abs_neg (g • z).re ▸ hg.2)]

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

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ∀ {a b c d f e : ℂ}, e ≠ 0 → (a / b = c / d * (e ^ 2)⁻¹ + f / e ↔ a * e ^ 2 / b = c / d + e * f)

Tactic:
intros

Goal state after:
A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
a✝ b✝ c✝ d✝ f✝ e✝ : ℂ
he✝ : e✝ ≠ 0
⊢ a✝ / b✝ = c✝ / d✝ * (e✝ ^ 2)⁻¹ + f✝ / e✝ ↔ a✝ * e✝ ^ 2 / b✝ = c✝ / d✝ + e✝ * f✝
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : |(T ^ ↑g 0 0 • ρ).re| ≤ 1 / 2
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = 1

Tactic:
simp only [Fin.isValue, ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re,
    abs_le, le_add_iff_nonneg_right, Int.cast_nonneg_iff, neg_add_le_iff_le_add,
    show (2⁻¹ : ℝ) + 2⁻¹ = 1 by norm_num] at hgzre

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ ↑g 0 0 ∧ ↑(↑g 0 0) ≤ 1
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
b : ℤ
⊢ 0 = ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))

Tactic:
by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

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

Goal state before:
pp: case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)

Tactic:
simpa [add_assoc] using! summable_left_one_div_linear_sub_one_div_linear z N (N + 1)

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

Goal state before:
pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
· have := G2Term_summable z
    rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this
    exact this.prod

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

Goal state before:
pp: z : ℍ
⊢ Δ (ModularGroup.T • z) *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) ↑z ^
        (-12) =
    Δ z

Tactic:
denom,

Goal state after:
z : ℍ
⊢ Δ (ModularGroup.T • z) *
      (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1 0) *
            ↑z +
          ↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) 1
              1)) ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ∑ m ∈ Icc (-↑N) ↑N, e2Summand m z =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
sum_Icc_of_even_eq_range (e2Summand_even z),

Goal state after:
z : ℍ
N : ℕ
⊢ 2 • ∑ m ∈ range (N + 1), e2Summand (↑m) z - e2Summand 0 z =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext z
    exact mul_div_cancel_left₀ (f z) (discriminant_ne_zero z)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im

Tactic:
hxnorm,

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 1 < 1 ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ |x.re| < 1 / 2

Tactic:
abs_lt,

Goal state after:
case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ -(1 / 2) < x.re ∧ x.re < 1 / 2
Module: Mathlib.NumberTheory.Modular

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

Tactic:
ext z
  constructor
  · rintro ⟨⟨z, hz⟩, h, rfl⟩
    exact ⟨hz.le, h.2, h.1.2, by simpa [Complex.normSq_eq_norm_sq] using h.1.1⟩
  · rintro ⟨hz, h1, h2, h3⟩
    have hz' : 0 < z.im := by
      apply hz.lt_of_ne
      contrapose! h3
      simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)
    exact ⟨⟨z, hz'⟩, ⟨⟨by simpa [Complex.normSq_eq_norm_sq], h2⟩, h1⟩, rfl⟩

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'
⊢ (⇑f ∣[k] (↑h)⁻¹) τ = (⇑f ∣[k] (↑h')⁻¹) τ

Tactic:
by
    obtain ⟨j, hj, hj'⟩ : ∃ g ∈ 𝒢, h' = h * g := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'
      exact ⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩
    simp [hj', SlashAction.slash_mul, SlashInvariantFormClass.slash_action_eq f j⁻¹ (inv_mem hj)]

Goal state after:
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)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
by
  simp_rw +instances [topologicalSpace_eq_iSup cofinite, isOpen_iSup_iff, isOpen_coinduced]
  exact fun S hS ↦ isOpen_forall_mem_of_principal hAopen hS

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ((x + y) * (x - y)) + emultiplicity 2 ↑d + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 * d)

pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

Tactic:
← Int.ofNat_mul_ofNat,

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ((x + y) * (x - y)) + emultiplicity 2 ↑d + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 (↑2 * ↑d)

x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2
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 : Y
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun p ↦ (inclusion R A hS p.1, id p.2)) (𝓝 (x', y)) (𝓝 (f (inclusion R A hS x', y)))

Tactic:
exact H S hS |>.tendsto ⟨x', y⟩

Goal state after:
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]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (Filter.pi fun i ↦ 𝓝 (inclusion (A i) (C i) hS (x' i)))
    (𝓝 (f (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x')))

Tactic:
nhds_eq_map_inclusion (hCopen _),

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]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (Filter.pi fun i ↦ Filter.map (inclusion (A i) (C i) hS) (𝓝 (x' i)))
    (𝓝 (f (Pi.map (fun j ↦ inclusion (A j) (C j) hS) x')))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
⊢ ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)

Tactic:
intro S

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
⊢ ∀ (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑ζ)| * mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
Units.norm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (↑1 * mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
u : Additive (𝓞 K)ˣ
left✝ : u ∈ ↑⊤
hu : ↑⟨(logEmbedding K).toIntLinearMap u, ⋯⟩ + logMap x ∈ ZSpan.fundamentalDomain B
⊢ u • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
rwa [Set.mem_preimage, logMap_unit_smul u hx]

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✝ : NumberField K
this : (powMonoidHom 2).range.index = 2
⊢ (unitsMulComplexConjInv K).range.index ∣ 2

Tactic:
refine this ▸ Subgroup.index_dvd_of_le ?_

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (powMonoidHom 2).range.index = 2
⊢ (powMonoidHom 2).range ≤ (unitsMulComplexConjInv K).range
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
⊢ (unitsMulComplexConjInv K).range.index ∣ 2

Tactic:
suffices (powMonoidHom 2 : _ →* torsion K).range.index = 2 by
    refine this ▸ Subgroup.index_dvd_of_le ?_
    rintro _ ⟨ζ, _, rfl⟩
    exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (powMonoidHom 2).range.index = 2
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_2
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|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
i✝ j✝ : Fin (rank K)
⊢ (reindex e₁ e₁) (of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))) i✝ j✝ =
    (of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0) i✝ j✝

Tactic:
simp only [ne_eq, reindex_apply, submatrix_apply, of_apply, Equiv.apply_symm_apply,
          Equiv.trans_apply, Fin.succAbove_zero, id_eq, finSuccEquiv_succ,
          Equiv.optionSubtype_symm_apply_apply_coe, f]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
⊢ (a : Quotient (MulAction.orbitRel ↥(Units.torsion K) ↑(integerSet K))) →
    ↥(Units.torsion K) ⧸ MulAction.stabilizer (↥(Units.torsion K)) a.out ≃ ↥(Units.torsion K)

Tactic:
by
        intro _
        simp_rw [integerSetTorsionSMul_stabilizer]
        exact QuotientGroup.quotientBot.toEquiv

Goal state after: