mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
← LSeries_eulerProduct_exp_log χ h₁,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ ‖cexp (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))) ^ 3 *
          cexp (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x

Tactic:
rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0

Tactic:
exact fun χ ↦ LFunction_ne_zero_of_one_le_re χ (.inr hs₁) <| Set.mem_ofPred.mp hs

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 4 ≠ 1

Tactic:
· decide

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val

Tactic:
have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
    lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (a * -(↑b / a)).valMinAbs.natAbs = b

Tactic:
· rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ 0 ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯ ↔ a.gcd ↑b ≠ 1

Tactic:
rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs
Module: Mathlib.Topology.Algebra.Module.Compact

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ Continuous ⇑(Fintype.linearCombination R Subtype.val)

Tactic:
simp only [Fintype.linearCombination, Finset.univ_eq_attach, LinearMap.coe_mk,
    AddHom.coe_mk]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ Continuous fun f ↦ ∑ i ∈ s.attach, f i • ↑i
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (i + 1) = ↑(s (i + 1))

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (i + 1)) = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : sZMod (p' + 2) (p' + 2 - 2) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
rw [sZMod_eq_s p'] at h

Goal state after:
p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (ω ^ 2 ^ (p' + 1)) ^ 2 = (-1) ^ 2

Tactic:
rw [ω_pow_eq_neg_one p' h]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mp
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ (∃ g, zpowers g = H) → DiscreteTopology ↥H

Tactic:
rintro ⟨g, rfl⟩

Goal state after:
case mp
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
g : G
⊢ DiscreteTopology ↥(zpowers g)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
rintro ⟨g, rfl⟩

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (mapGL ℝ) g • ∞ ∈ Set.range (OnePoint.map Rat.cast)
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_4
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cofinite = Filter.coprodᵢ fun x ↦ cofinite

pp: case e'_5
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cocompact (Fin 2 → ℝ) = Filter.coprodᵢ fun x ↦ cocompact ℝ

Tactic:
· rw [coprodᵢ_cofinite]

Goal state after:
case e'_5
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cocompact (Fin 2 → ℝ) = Filter.coprodᵢ fun x ↦ cocompact ℝ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto (mB ∘ fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))

Tactic:
have hf₁ : Tendsto f₁ cofinite (cocompact _) :=
    cocompact_ℝ_to_cofinite_ℤ_matrix.comp Subtype.coe_injective.tendsto_cofinite

Goal state after:
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ cd]
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
⊢ Tendsto (mB ∘ fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite
    (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
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
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
by
  -- Extract a bound for large `im τ` using `hf_infty`.
  obtain ⟨D, hD, hf_infinity⟩ := hf_infinity.exists_pos
  rw [IsBigOWith, atImInfty, eventually_comap, eventually_atTop] at hf_infinity
  obtain ⟨y, hy⟩ := hf_infinity
  simp only [Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le] at hy
  -- Extract a bound for the rest of `𝒟` using continuity and compactness.
  have hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / (im τ) ^ t) (truncatedFundamentalDomain y) := by
    apply (hf_cont.norm.div ?_ fun τ ↦ by positivity).continuousOn
    exact continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero
  obtain ⟨E, hE⟩ : ∃ E, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / (im τ) ^ t ≤ E := by
    simpa [norm_mul, norm_norm, Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le]
      using (isCompact_truncatedFundamentalDomain y).exists_bound_of_continuousOn hfm
  -- Put the two bounds together.
  refine ⟨max D E, fun τ hτ ↦ ?_⟩
  rcases le_total y (im τ) with hτ' | hτ'
  · exact (hy _ hτ' _ rfl).trans <| mul_le_mul_of_nonneg_right (le_max_left ..) (by positivity)
  · rw [← div_le_iff₀ (by positivity)]
    exact (hE τ ⟨hτ, hτ'⟩).trans (le_max_right _ _)

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

Goal state before:
pp: k : ℤ
hk : k < 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ 1 • f = 0

Tactic:
simpa [← FunLike.coe_zero_iff] using levelOne_neg_weight_eq_zero hk f

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

Goal state after:
case inl
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = τ.re ∧ 0 ≤ τ.re
⊢ 3 ≤ 4 * τ.im ^ 2

case inr
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = -τ.re ∧ τ.re < 0
⊢ 3 ≤ 4 * τ.im ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
hk' : 2 < ↑k
⊢ ∀ (i : Fin 2 → ℤ),
    ‖eisSummand k i (ModularGroup.T ^ (↑N * n) • z)‖ ≤
      r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖i‖ ^ (-k)

Tactic:
· intro x
    simp_rw [eisSummand, norm_zpow]
    exact_mod_cast
      summand_bound_of_mem_verticalStrip (lt_trans two_pos hk').le x two_pos
      (verticalStrip_anti_right N hz hn)

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
⊢ qExpansion h ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) =
    qExpansion h ⇑f * qExpansion h ⇑g

Tactic:
simpa [DirectSum.of_mul_of] using! ModularForm.qExpansion_mul hh hΓ f g

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ (g • z).im = z.im

pp: g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
hc : 0 ≤ ↑g 1 0
⊢ (g • z).im = z.im

Tactic:
· -- TODO: `wlog` leaves junk copies of variables in scope
    simpa using @this (-g) z (-g) z hz (by simpa using hg)
      (by simpa using hden) (by simpa using (not_le.mp hc).le)

Goal state after:
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
hc : 0 ≤ ↑g 1 0
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed 𝒟

Tactic:
by
  refine .inter (.preimage (by fun_prop) isClosed_Ici) ?_
  exact isClosed_le (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
t : ℝ≥0
⊢ 0 < (↑x + ↑↑t * Complex.I).im

Tactic:
by
      simpa using! add_pos_of_pos_of_nonneg x.coe_im_pos t.property

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

Goal state before:
pp: Γ : 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 : ↑k + 1 < s.re
⊢ ↑k + 1 < s.re

Tactic:
by exact_mod_cast hs

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
⊢ HasFDerivAt (↑(polarCoordReal K).symm) (FDerivPolarCoordRealSymm K x) x

Tactic:
by
  classical
  exact (hasFDerivAt_id x.1).prodMap x (hasFDerivAt_pi_polarCoord_symm x.2)

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : y ∈ fundamentalCone K ∧ mixedEmbedding.norm y ≤ 1
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1

Tactic:
← normAtAllPlaces_mem_fundamentalCone_iff,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hy₁ : mixedSpaceOfRealSpace (normAtAllPlaces y) ∈ fundamentalCone K ∧ mixedEmbedding.norm y ≤ 1
hy₂ : normAtAllPlaces y = normAtAllPlaces x
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(intNorm ↑((idealSetEquiv K J) a)) = mixedEmbedding.norm ↑a

Tactic:
rw [intNorm_coe, idealSetEquiv_apply]

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 : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n) ∧ ↑J ∣ ↑x✝ ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = n

Tactic:
by rw [and_comm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ.pi fun i ↦ (expMap_single i).target) = Set.univ.pi fun x ↦ Set.Ioi 0

Tactic:
expMap_single

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

Goal state before:
pp: K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
⊢ maximalRealSubfield K ≤ E

Tactic:
by_contra! h

Goal state after:
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
⊢ False
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
i : { w // w ≠ w₀ }
| w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
rw [if_neg i.prop]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
i : { w // w ≠ w₀ }
| w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup ≤ (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup

Tactic:
span_basisOfIsMaxRank hu,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u))) ≤
    (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

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

Tactic:
nth_rewrite 2 [← pow_one pB.gen]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = pB.gen ^ 1
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₀
w i : { i // i ≠ w₀ }
| (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i

Tactic:
rw [if_neg i.prop]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w✝ : InfinitePlace K
hw : w✝ ≠ w₀
w i : { i // i ≠ w₀ }
| x ↑i • (completeBasis K) ↑i
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup.relIndex
        (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
span_basisOfIsMaxRank hu,

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))).relIndex
        (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
⊢ ζ ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val = ζ ^ (↑((galEquivZMod n K) σ)).val

Tactic:
apply FaithfulSMul.algebraMap_injective F K

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := ⋯
⊢ (algebraMap F K) (ζ ^ (↑((galEquivZMod m F) (σ.restrictNormal F))).val) =
    (algebraMap F K) (ζ ^ (↑((galEquivZMod n K) σ)).val)