mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
h₀ : ¬w 1 = 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

Tactic:
simp [h₀, ht, mul_assoc]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ (fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯)
      ((fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p) p) =
    p

Tactic:
induction p using ind with

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

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Monoid G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ (-a + a) ∣[k] g = 0

Tactic:
neg_add_cancel,

Goal state after:
β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Monoid G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ 0 ∣[k] g = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
x✝ : Fin 2
⊢ (fun g ↦ ↑g 1) ⟨A, det_A_1⟩ x✝ = cd x✝

Tactic:
simp [A]

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

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ (Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)).IsParabolic

Tactic:
GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)

Goal state after:
case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k k_1 k_2 : ℤ
inst✝ : Γ.HasDetPlusMinusOne
f : ModularForm Γ k_1
g : ModularForm Γ k_2
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((f.mul g.toSlashInvariantForm).toFun ∣[k_1 + k_2] γ)

Tactic:
simpa [mul_slash] using! ((f.bdd_at_cusps' hc γ hγ).mul (g.bdd_at_cusps' hc γ hγ)).smul _

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
| Real.exp (-a * τ.im)

Tactic:
← one_mul (Real.exp _)

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
| 1 * Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case h₁
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ (g • τ).im ≤ max τ.im (1 / τ.im)

Tactic:
rw [im_smul_eq_div_normSq, denom_apply]

Goal state after:
case h₁
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg : g • τ ∈ 𝒟
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| 0

Tactic:
rw [show 0 = 0 * (2 * π / h) by simp]

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| 0 * (2 * π / h)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case e_f
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I * (f τ / 𝕢 h ↑τ ^ (n + 1))) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f τ)

Tactic:
pow_succ

Goal state after:
case e_f
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I * (f τ / (𝕢 h ↑τ ^ n * 𝕢 h ↑τ))) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f τ)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ (fun τ ↦ f τ - valueAtInfty f) =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)

Tactic:
have := hfbdd.comp_tendsto tendsto_comap_im_ofComplex
  convert!
    (hfper.exp_decay_sub_of_bounded_at_inf hh
          (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0)) fun z hz ↦ by
            simpa using (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩))
          this).comp_tendsto
      tendsto_coe_atImInfty
  simpa [cuspFunction] using
    (cuspFunction_apply_zero hh (analyticAt_cuspFunction_zero hh hfper hfhol hfbdd) hfper).symm

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c ^ 2 ≤ 4
⊢ |↑g 1 0| ≤ 1

Tactic:
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this
    replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
    rwa [sq_le_sq, abs_one] at this

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

Goal state before:
pp: case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑f ^ n * qExpansion h ⇑f = qExpansion h ⇑f ^ (n + 1)

Tactic:
pow_succ

Goal state after:
case succ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n
⊢ qExpansion h ⇑f ^ n * qExpansion h ⇑f = qExpansion h ⇑f ^ n * qExpansion h ⇑f
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case 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
hzre : |z.re| = 1 / 2
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
rw [abs_eq (by norm_num)] at hzre
      rcases hzre with hzre | hzre <;> [norm_num [hzre] at this; skip]
      rw [h, zpow_neg_one] at hg'
      exact .inr <| .inl ⟨hg', eq_of_re_of_norm (by norm_num [hzre, ρ]) (by rw [hz', norm_ρ])⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
⊢ (g • z).im = z.im

Tactic:
rcases cases_c_zero hz hg hc with h | h | h | h <;>
    rcases h with ⟨(rfl | rfl), -⟩ <;>
    simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

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

Goal state before:
pp: k : ℕ
z : ℍ
⊢ iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

Tactic:
iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)

Goal state after:
k : ℕ
z : ℍ
⊢ ∑' (n : ℕ), iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

case hsum
k : ℕ
z : ℍ
⊢ ∀ t ∈ ℍₒ, Summable fun n ↦ cexp (2 * ↑π * I * t) ^ n

case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 ⇑f = qExpansion 1 Δ * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

Tactic:
rw [show (f : ℍ → ℂ) = discriminant * (toCuspForm f hcusp).discriminantEquiv from
      (discriminant_mul_discriminantEquiv (toCuspForm f hcusp)).symm, ← CuspForm.coe_discriminant]

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 (⇑CuspForm.discriminant * ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))) =
    qExpansion 1 ⇑CuspForm.discriminant * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ 0 < z.im

Tactic:
apply hz.lt_of_ne

Goal state after:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ 0 ≠ z.im
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
K L : Set α
hK : IsCompact K
⊢ IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
hL

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
⊢ IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
hL

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (↑p * b * ∑ x ∈ range p, a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Tactic:
simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1 + (p - 1 - x)) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, ↑p * b * a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
eq_add_of_sub_eq' hk

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hx : ¬↑p ∣ y
k : R
hk : x - y = ↑p * k
⊢ ¬↑p ^ 2 ∣ ∑ i ∈ range p, (y + ↑p * k) ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
hpn : 2 ∣ k
⊢ 2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1

Tactic:
pow_succ

Goal state after:
case succ.hn
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
hpn : 2 ∣ k
⊢ 2 ^ multiplicity 2 (n + 1) * 2 ∣ n + 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (x ^ 2 - y ^ 2) % 4 = 0

Tactic:
Int.sub_emod,

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (x ^ 2 % 4 - y ^ 2 % 4) % 4 = 0
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)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ)

Tactic:
by
  rw [continuous_dom]
  intro S hS
  set T := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
  have hT : 𝓕₂ ≤ 𝓟 T := by
    rw [le_principal_iff] at hS ⊢
    exact inter_mem (hf hS) hφ
  have hf' : Tendsto f (𝓟 T) (𝓟 S) := by aesop
  have hφ' : ∀ᶠ j in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j) := by aesop
  have key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS =
      inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ' := rfl
  rw [key]
  exact continuous_inclusion _ |>.comp <|
    continuous_rng_of_principal.mpr <|
    continuous_pi fun j ↦ φ_cont j |>.comp <| continuous_eval (f j)

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

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

Tactic:
rw [← setLIntegral_univ f, ← setLIntegral_congr (polarCoordReal_symm_target_ae_eq_univ K),
    lintegral_image_eq_lintegral_abs_det_fderiv_mul volume
      (polarCoordReal K).open_target.measurableSet
      (fun x _ ↦ (hasFDerivAt_polarCoordReal_symm K x).hasFDerivWithinAt)
      (polarCoordReal K).symm.injOn f]
  refine setLIntegral_congr_fun (polarCoordReal K).open_target.measurableSet (fun x hx ↦ ?_)
  simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : polarSpace K) in (polarSpaceCoord K).target, (∏ w, x.1 ↑w) • f (↑(polarSpaceCoord K).symm x) =
    ∫ (x : mixedSpace K), f x

Tactic:
by
  rw [← (volume_preserving_homeoRealMixedSpacePolarSpace K).setIntegral_preimage_emb
    (homeoRealMixedSpacePolarSpace K).measurableEmbedding,
    ← mixedEmbedding.integral_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.CMField

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

Tactic:
rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]

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

Goal state before:
pp: 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)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
have : Finite (AdjoinRoot P) := Module.finite_of_finite K

Goal state after:
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)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
⊢ False

Tactic:
refine (prime_of_normalized_factor _ hP).not_isUnit (squarefree_cyclotomic n K P ?_)

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this✝ : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H✝ : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero ↑n
hP : P ∈ normalizedFactors (cyclotomic n K)
⊢ P * P ∣ cyclotomic n K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : p = 2
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

pp: case neg
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : ¬p = 2
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
· cases k with
    | zero =>
      rw [h, zero_add, pow_one] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two, h, Int.ofNat_two, Associated.neg_left_iff]
    | succ n =>
      rw [h, add_assoc, one_add_one_eq_two] at hK hζ
      rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]

Goal state after:
case neg
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
h : ¬p = 2
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p
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
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main :
  (𝒑.primesOver (𝓞 K)).ncard * ((span {hζ.toInteger - 1}).ramificationIdx ℤ * (span {hζ.toInteger - 1}).inertiaDeg ℤ) =
    Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
inertiaDeg_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
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : (𝒑.primesOver (𝓞 K)).ncard * ((span {hζ.toInteger - 1}).ramificationIdx ℤ * 1) = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1