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

Goal state before:
pp: g : SL(2, ℤ)
⊢ g • I = I ↔ g ∈ {1, -1, S, -S}

Tactic:
constructor

Goal state after:
case mp
g : SL(2, ℤ)
⊢ g • I = I → g ∈ {1, -1, S, -S}

case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S, -S} → g • I = I
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
⊢ g • ρ = ρ ↔ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

Tactic:
constructor

Goal state after:
case mp
g : SL(2, ℤ)
⊢ g • ρ = ρ → g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_a.e_a
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑m * ↑z)) ^ ↑n =
    ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * ↑z) ^ (↑m * ↑n)

Tactic:
← Complex.exp_nat_mul

Goal state after:
case e_a.e_a
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) =
    ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (↑(↑m * ↑n) * (2 * ↑π * I * ↑z))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed (UpperHalfPlane.coe '' 𝒟)

Tactic:
by
  rw [coe_fd]
  have : IsClosed {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1/2} := by
    refine .inter ?_ (.inter ?_ ?_)
    · exact isClosed_le continuous_const Complex.continuous_im
    · exact isClosed_le continuous_const continuous_norm
    · exact isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const
  convert! this using 1
  ext x
  refine ⟨fun ⟨him, hre, hnorm⟩ ↦ ⟨him.le, hre, hnorm⟩, fun ⟨him, hre, hnorm⟩ ↦ ⟨?_, hre, hnorm⟩⟩
  exact him.lt_of_ne' <| by grind [abs_re_eq_norm]

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

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

Tactic:
by
  convert! tsum_zero
  exact tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z _

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ x ∈ 𝒟ᵒ

Tactic:
constructor

Goal state after:
case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < normSq ↑x

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

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

Tactic:
constructor

Goal state after:
case mp
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y → z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} ∧
    Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
constructor

Goal state after:
case left
y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

case right
y : ℝ
⊢ Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ 1 = fun x ↦ ∏ i, 1

Tactic:
ext

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
x✝ : ℍ
⊢ 1 x✝ = ∏ i, 1
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range f = 0

Tactic:
ext

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x✝ : ℍ
⊢ (ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range f) x✝ = 0 x✝
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ { coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
      { coe := I * ↑t, coe_im_pos := ⋯ }

Tactic:
ext

Goal state after:
case e_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
        { coe := I * ↑t, coe_im_pos := ⋯ })
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
⊢ p ^ 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)

Tactic:
convert! this; abel

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 0) } = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 0) }.toCompletion = toCompletion 0
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 1) } = 1

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) 1) }.toCompletion = toCompletion 1
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x y : K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) (x + y)) } =
    { toCompletion := ↑(WithAbs.toAbs (↑v) x) } + { toCompletion := ↑(WithAbs.toAbs (↑v) y) }

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x y : K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) (x + y)) }.toCompletion =
    ({ toCompletion := ↑(WithAbs.toAbs (↑v) x) } + { toCompletion := ↑(WithAbs.toAbs (↑v) y) }).toCompletion
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x y : K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) (x * y)) } =
    { toCompletion := ↑(WithAbs.toAbs (↑v) x) } * { toCompletion := ↑(WithAbs.toAbs (↑v) y) }

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x y : K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) (x * y)) }.toCompletion =
    ({ toCompletion := ↑(WithAbs.toAbs (↑v) x) } * { toCompletion := ↑(WithAbs.toAbs (↑v) y) }).toCompletion
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
rw [pow_one]

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ↑p ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
⊢ DFunLike.coe ∘ mulSingle A i = Pi.mulSingle i

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
x✝¹ : G i
x✝ : ι
⊢ (DFunLike.coe ∘ mulSingle A i) x✝¹ x✝ = Pi.mulSingle i x✝¹ x✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i : ι
⊢ mulSingle A i 1 = 1

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i : ι), OneMemClass (S i) (G i)
i i✝ : ι
⊢ (mulSingle A i 1) i✝ = 1 i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulOneClass (G i)
inst✝¹ : ∀ (i : ι), OneMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r s : G i
⊢ mulSingle A i (r * s) = mulSingle A i r * mulSingle A i s

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulOneClass (G i)
inst✝¹ : ∀ (i : ι), OneMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r s : G i
i✝ : ι
⊢ (mulSingle A i (r * s)) i✝ = (mulSingle A i r * mulSingle A i s) i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
⊢ mulSingle A i r⁻¹ = (mulSingle A i r)⁻¹

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
i✝ : ι
⊢ (mulSingle A i r⁻¹) i✝ = (mulSingle A i r)⁻¹ i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r s : G i
⊢ mulSingle A i (r / s) = mulSingle A i r / mulSingle A i s

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r s : G i
i✝ : ι
⊢ (mulSingle A i (r / s)) i✝ = (mulSingle A i r / mulSingle A i s) i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (G i)
i : ι
r : G i
n : ℕ
⊢ mulSingle A i (r ^ n) = mulSingle A i r ^ n

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (G i)
i : ι
r : G i
n : ℕ
i✝ : ι
⊢ (mulSingle A i (r ^ n)) i✝ = (mulSingle A i r ^ n) i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
n : ℤ
⊢ mulSingle A i (r ^ n) = mulSingle A i r ^ n

Tactic:
ext

Goal state after:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
n : ℤ
i✝ : ι
⊢ (mulSingle A i (r ^ n)) i✝ = (mulSingle A i r ^ n) i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
⊢ ⟨fun i ↦ ↑(x i), ⋯⟩ * ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ = 1

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
i✝ : ι
⊢ (⟨fun i ↦ ↑(x i), ⋯⟩ * ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩) i✝ = 1 i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
⊢ ⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ * ⟨fun i ↦ ↑(x i), ⋯⟩ = 1

Tactic:
ext

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ (Submonoid.ofClass (B i)).units
i✝ : ι
⊢ (⟨fun i ↦ ↑(x i)⁻¹, ⋯⟩ * ⟨fun i ↦ ↑(x i), ⋯⟩) i✝ = 1 i✝
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
T : Set ι
⊢ ∀ (hS : 𝓕 ≤ 𝓟 T),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
hT

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
    ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hT)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
T : Set ι
⊢ ∀ (hS : 𝓕 ≤ 𝓟 T),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
hT

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
    ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hT)
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ Set.range ⇑(basisOfIsMaxRank hu) = ⇑(logEmbedding K) '' ⇑Additive.toMul ⁻¹' Set.range u

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
x✝ : logSpace K
⊢ x✝ ∈ Set.range ⇑(basisOfIsMaxRank hu) ↔ x✝ ∈ ⇑(logEmbedding K) '' ⇑Additive.toMul ⁻¹' Set.range u
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))

Tactic:
rw [Subgroup.toAddSubgroup_closure, AddMonoidHom.map_closure, ← span_int_eq_addSubgroupClosure]
  congr; ext; simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ ×ˢ Set.univ.pi fun x ↦ ↑polarCoord.symm '' polarCoord.target) =ᵐ[volume.prod volume] Set.univ ×ˢ Set.univ

Tactic:
← Set.piMap_image_univ_pi

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.univ ×ˢ ((Pi.map fun x ↦ ↑polarCoord.symm) '' Set.univ.pi fun x ↦ polarCoord.target) =ᵐ[volume.prod volume]
    Set.univ ×ˢ Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 0 = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 0 x✝ = 0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 1 = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 1 x✝ = 0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (polarSpaceCoord K).target =
    (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ x✝ ∈ (polarSpaceCoord K).target ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = (logEmbedding K) (Additive.ofMul u)

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x✝ : { w // w ≠ w₀ }
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) x✝ = (logEmbedding K) (Additive.ofMul u) x✝
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:
← (volume_preserving_homeoRealMixedSpacePolarSpace K).setIntegral_preimage_emb
    (homeoRealMixedSpacePolarSpace K).measurableEmbedding,

Goal state after:
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 : realMixedSpace K) in ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹' (polarSpaceCoord K).target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : mixedSpace K), f x
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
⊢ logMap (ζ • x) = logMap x

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ logMap (ζ • x) x✝ = logMap x x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ logMap (c • 1) = 0

Tactic:
ext

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ logMap (c • 1) x✝ = 0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

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

Tactic:
mul_comm (finrank ℚ K : ℝ) _,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log |c| - Real.log |c| * ↑(finrank ℚ K) * (↑(finrank ℚ K))⁻¹) = 0 x✝
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
⊢ logMap x = logMap y

Tactic:
ext

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₀ }
⊢ logMap x x✝ = logMap y x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
h : ∀ (x : mixedSpace K) (w : InfinitePlace K), w.IsComplex → 0 ≤ normAtComplexPlaces x w
x : realSpace K
x✝ : x ∈ ⇑mixedSpaceOfRealSpace ⁻¹' A ∩ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
hx₁ : normAtComplexPlaces (mixedSpaceOfRealSpace x) ∈ normAtComplexPlaces '' A
hx₂ : x ∈ Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ici 0
w : InfinitePlace K
hw : w.IsComplex
⊢ 0 ≤ x w

Tactic:
simpa [if_neg (not_isReal_iff_isComplex.mpr hw)] using hx₂ w (Set.mem_univ w)

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
· rw [Set.mem_ofPred_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]
    exact ⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩

Goal state after: