mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
this : Dense ↑⊤ ∨ ∃ a, zpowers a = ⊤
hA : DiscreteTopology ↥⊤
h : Dense ↑⊤
⊢ ∃ g, zpowers g = ⊤

Tactic:
have : DiscreteTopology G := by rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
this✝ : Dense ↑⊤ ∨ ∃ a, zpowers a = ⊤
hA : DiscreteTopology ↥⊤
h : Dense ↑⊤
this : DiscreteTopology G
⊢ ∃ g, zpowers g = ⊤
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ n • g • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
hg.smul_eq_self_iff.mpr rfl,

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
⊢ Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)

Tactic:
intro k

Goal state after:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
k : SL(2, ℤ)
⊢ k ∈ Γ(N) → k ∈ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsBoundedAt f k ↔ c.IsBoundedAt (f ∣[k] g) k

Tactic:
IsBoundedAt,

Goal state after:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = g • c → IsBoundedAtImInfty (f ∣[k] g_1)) ↔ c.IsBoundedAt (f ∣[k] g) k
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = g • c → IsBoundedAtImInfty (f ∣[k] g_1)) ↔ c.IsBoundedAt (f ∣[k] g) k

Tactic:
IsBoundedAt,

Goal state after:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = g • c → IsBoundedAtImInfty (f ∣[k] g_1)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = c → IsBoundedAtImInfty ((f ∣[k] g) ∣[k] g_1)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods ≤ 𝒢.periods

Tactic:
intro k

Goal state after:
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
k : R
⊢ k ∈ 𝒢.strictPeriods → k ∈ 𝒢.periods
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
⊢ IsCusp ∞ 𝒢 → 0 < 𝒢.strictWidthInfty

Tactic:
rintro ⟨g, hgg, hgp, hgi⟩

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ 0 < 𝒢.strictWidthInfty
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ IsCusp ∞ 𝒢

Tactic:
refine ⟨upperRightHom h, 𝒢.mem_strictPeriods_iff.mp h𝒢, ?_, smul_infty_eq_self_iff.mpr rfl⟩
  exact (GeneralLinearGroup.isParabolic_iff_of_upperTriangular rfl).mpr ⟨rfl, hh.ne'⟩

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) ⊤ =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}

Tactic:
← SpecialLinearGroup.SL2Z_generators,

Goal state after:
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Subgroup.closure {S, T}) =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ I ∈ 𝒟

Tactic:
by
  constructor <;> norm_num

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

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))
⊢ ↑v ᵥ* ↑γ⁻¹ ∈ gammaSet N r a

Tactic:
have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
      rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this
      simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
        map_inv, mul_inv_cancel, SpecialLinearGroup.coe_one, vecMul_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
⊢ 3 ≤ 4 * τ.im ^ 2

Tactic:
cases abs_cases τ.re <;> nlinarith [h.2]

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

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ (fun τ ↦ ‖petersson k (⇑f ∣[k] g) (⇑f' ∣[k] g) τ‖) =O[atImInfty] fun z ↦ z.im ^ k

Tactic:
simpa [petersson, Real.norm_of_nonneg (_ : ℍ).im_pos.le]
    using (bdd_at_infty_slash f g).norm_left.mul (bdd_at_infty_slash f' g).norm_left
      |>.mul (isBigO_refl ..)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : ↑|b| ≤ ↑1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
Int.cast_le,

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : |b| ≤ 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: n : ℕ+
x : ↥(↑n).divisorsAntidiagonal
⊢ ↑(divisorsAntidiagonalFactors n x).1 * ↑(divisorsAntidiagonalFactors n x).2 = ↑n

Tactic:
simp [divisorsAntidiagonalFactors, (Nat.mem_divisorsAntidiagonal.mp x.2).1]

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:
symmetricIoo,

Goal state after:
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
⊢ { filter := Filter.map (fun g ↦ Ioo (-g) g) atTop }.filter ≤ atTop
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : ↑|↑g 0 0| ≤ ↑1
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
Int.cast_le,

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑g 0 0| ≤ 1
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
⊢ D2 (A * B) = D2 A ∣[2] B + D2 B

Tactic:
ext z
  simp only [D2, mul_assoc, coe_mul, map_mul, ← mul_div, SL_slash_def,
    ModularGroup.sl_moeb, Int.reduceNeg, zpow_neg, Pi.add_apply, ← mul_add, mul_eq_mul_left_iff,
    I_ne_zero, or_false, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero]
  have hd : (A.1 * B.1) 1 0 * denom (φ B) z - B 1 0 * denom (φ A * φ B) z = A 1 0 := by
    simpa [sub_eq_iff_eq_add] using denom_aux A B z
  have : denom A (num B z / denom B z) = denom A ↑(B • z) := by
    simp [specialLinearGroup_apply, denom, num]
  rw [(by intros; field_simp : ∀ {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) (denom_ne_zero B z)]
  simp only [pow_two, ← mul_assoc, denom_cocycle A B z.im_ne_zero, this,
    ModularGroup.sl_moeb, ← hd]
  field_simp [denom_ne_zero A (toGL (φ B) • z)]
  ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl.inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
h,

Goal state after:
case inr.inr.inl.inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ 1 * S
hSre : (S • z).re = -z.re
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr.inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
h,

Goal state after:
case inr.inr.inr.inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ (-1) * S
hSre : (S • z).re = -z.re
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
hzre : z.re = -(1 / 2)
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ √(normSq ↑z) = ‖↑(1 +ᵥ ρ)‖

Tactic:
h,

Goal state after:
case hnorm
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ √1 = ‖↑(1 +ᵥ ρ)‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (c : (r : ℕ) × ↑(gammaSet 1 r 0)), eisSummand (↑k) (↑c.snd) z =
    riemannZeta ↑k * ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z

Tactic:
Summable.tsum_sigma ?hsumm,

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑⟨b, c⟩.snd) z =
    riemannZeta ↑k * ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z

case hsumm
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun c ↦ eisSummand (↑k) (↑c.snd) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im

Tactic:
obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ
  use γ
  nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hxy
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
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ ↑p ∣ x ^ p ^ a - y ^ p ^ a

pp: case succ.hx
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
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ ¬↑p ∣ x ^ p ^ a

Tactic:
· rw [← geom_sum₂_mul]
      exact dvd_mul_of_dvd_right hxy _

Goal state after:
case succ.hx
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
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ ¬↑p ∣ x ^ p ^ a
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : ¬IsUnit a
⊢ {v | Valued.v (a v) ≠ 1}.Infinite

Tactic:
contrapose! ha

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : {v | Valued.v (a v) ≠ 1}.Finite
⊢ IsUnit a
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : {v | Valued.v (a v) ≠ 1}.Finite
⊢ IsUnit a

Tactic:
isUnit_iff

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : {v | Valued.v (a v) ≠ 1}.Finite
⊢ (∀ (v : HeightOneSpectrum R), a v ≠ 0) ∧ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, Valued.v (a v) = 1
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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ (∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S) (S_1 : Set ι) (hS_1 : cofinite ≤ 𝓟 S_1),
      Continuous[instTopologicalSpaceProd, inst✝]
        ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hS_1))) ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
refine ⟨fun H S hS ↦ H S hS S hS, fun H S hS T hT ↦ ?_⟩

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)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))
S : Set ι
hS : cofinite ≤ 𝓟 S
T : Set ι
hT : cofinite ≤ 𝓟 T
⊢ Continuous[instTopologicalSpaceProd, inst✝] ((f ∘ Prod.map (inclusion R A hS) id) ∘ Prod.map id (inclusion R' A' hT))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : (𝓞 K)ˣ
⊢ x✝ • 0 = 0

Tactic:
simp_rw [unitSMul_smul, mul_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • x = 0

Tactic:
h,

Goal state after:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • x = 0

Tactic:
by rw [h, smul_zero]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ (normAtPlace w) (↑(mixedEmbedding.polarCoord K).symm x) = ‖x.1 ⟨w, hw⟩‖

Tactic:
simp [normAtPlace_apply_of_isReal hw]

Goal state after:
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 : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫⁻ (x : mixedSpace K), f x

Tactic:
← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).lintegral_comp_emb
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫⁻ (a : realMixedSpace K), f ((mixedSpaceToRealMixedSpace K).symm a) ∂volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

Tactic:
h,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) y) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h : indexRealUnits K = 2
⊢ (unitsMulComplexConjInv K).range.index = 1

Tactic:
h,

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : 2 * (unitsMulComplexConjInv K).range.index = 2
h : indexRealUnits K = 2
⊢ (unitsMulComplexConjInv K).range.index = 1
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2

Tactic:
h,

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : indexRealUnits K * 1 = 2
h : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | ∀ (w : InfinitePlace K), 0 ≤ x w}

pp: case refine_1.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}

pp: case refine_1.refine_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}

Tactic:
· exact fun w ↦ normAtPlace_nonneg w y

Goal state after:
case refine_1.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≠ 0}

case refine_1.refine_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : mixedSpace K
h₃ : y ∈ {x | mixedEmbedding.norm x ≤ 1}
h₁ : y ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
h₂ : y ∉ {x | mixedEmbedding.norm x = 0}
⊢ normAtAllPlaces y ∈ {x | mixedEmbedding.norm (mixedSpaceOfRealSpace x) ≤ 1}