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

Goal state before:
pp: case h.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : k < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

pp: case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

pp: case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
· -- `k < 3`: direct case-by-case check
    interval_cases k
    · simpa using! levelOne_weight_zero_rank_one
    · grind
    · simpa [Nat.ModEq] using levelOne_weight_two_rank_zero

Goal state after:
case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
this : k ∈ Finset.filter Even (Finset.Icc 3 11)
⊢ 1 + 0 = ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
fin_cases this

Goal state after:
case h.inr.inl.«0»
ihn :
  ∀ m < 3 + 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even (3 + 1)
hk : 3 ≤ 3 + 1 ∧ 3 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 ≡ 2 [MOD 12] then (3 + 1) / 12 else (3 + 1) / 12 + 1)

case h.inr.inl.«1»
ihn :
  ∀ m < 3 + 1 + 1 + 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even (3 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1) / 12 + 1)

case h.inr.inl.«2»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even (3 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1 + 1 + 1) / 12 + 1)

case h.inr.inl.«3»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12
      else (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12 + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑i) - 1 / (↑m * ↑z + ↑i + 1)

Tactic:
apply (summable_left_one_div_linear_sub_one_div_linear z i (i + 1)).congr

Goal state after:
z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ ∀ (b : ℤ), 1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑(i + 1)) = 1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑i + 1)
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 ℋ)
⊢ ((∏ q, quotientFunc f q) ∣[k * ↑(Fintype.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ) =O[atImInfty] 1

Tactic:
← Finset.card_univ,

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 ℋ)
⊢ ((∏ q, quotientFunc f q) ∣[k * ↑Finset.univ.card] γ) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ ∀ t ∈ Set.Ioi 0,
    HasSum
      (fun i ↦
        if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
      ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)

Tactic:
intro t

Goal state after:
case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
⊢ t ∈ Set.Ioi 0 →
    HasSum
      (fun i ↦
        if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
      ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)
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)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤
    TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced DFunLike.coe inferInstance)

Tactic:
inclusion_eq_id R A (𝓟 S),

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤
    TopologicalSpace.coinduced id (TopologicalSpace.induced DFunLike.coe inferInstance)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
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:
exact fun h => hx (hp.dvd_of_dvd_pow h)

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

Goal state before:
pp: case e'_5
Γ : 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 : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / s.Gammaℂ * ↑(h Γ) ^ (-s))

Tactic:
rw [Gammaℂ, ← div_div, ← div_div, div_self two_ne_zero, one_div, cpow_neg (2 * _), inv_inv,
      ← ofReal_ofNat, mul_cpow_ofReal_nonneg two_pos.le Real.pi_pos.le]

Goal state after:
case e'_5
Γ : 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 : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (↑2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

Tactic:
exact fun h => hx (hp.dvd_of_dvd_pow h)

Goal state after:
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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
⊢ (Support R k).Finite

Tactic:
apply Set.Finite.subset this

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
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hd' : d ≠ 0
this : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
⊢ Support R k ⊆ {v | (valuation K v) ((algebraMap R K) d) < 1}
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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
| n + 1

Tactic:
hk

Goal state after:
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) * k
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n

Tactic:
convert! Int.two_pow_sub_pow hxy hx hn using 2

Goal state after:
case e'_3.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 n = emultiplicity 2 ↑n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

pp: case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
· iterate 3 rw [← Int.natCast_emultiplicity]
    simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]
    rw [← Int.natCast_dvd_natCast] at hx
    rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy
    convert! Int.two_pow_sub_pow hxy hx hn using 2
    rw [← Int.natCast_emultiplicity]
    rfl

Goal state after:
case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
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)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ (QuotientGroup.mk' (torsion K)).ker).index *
      (QuotientGroup.mk' (torsion K)).range.index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0

Tactic:
QuotientGroup.ker_mk',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index * (QuotientGroup.mk' (torsion K)).range.index
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    (span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))).toAddSubgroup.index ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝² x✝¹ : (𝓞 K)ˣ
x✝ : mixedSpace K
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝ : Field K
x✝² x✝¹ : (𝓞 K)ˣ
x✝ : mixedSpace K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(x✝² * x✝¹)) * x✝ =
    (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝²) * ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝¹) * x✝)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : mixedSpace K
⊢ 1 • x✝ = x✝

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝ : Field K
x✝ : mixedSpace K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑1) * x✝ = x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

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

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝ : Field K
x✝ : (𝓞 K)ˣ
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑x✝) * 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
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) (u • x) ≠ 0

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h✝ : x ≠ 0
w : InfinitePlace K
h : (normAtPlace w) x ≠ 0
⊢ (normAtPlace w) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * x) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ u • (mixedEmbedding K) ↑x = (mixedEmbedding K) ↑y ↔ ↑u * x = y

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ↑x = (mixedEmbedding K) ↑y ↔ ↑u * x = y
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm (u • x) = mixedEmbedding.norm x

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * x) = mixedEmbedding.norm x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ logMap (u • x) = (logEmbedding K) (Additive.ofMul u) + logMap x

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
u : (𝓞 K)ˣ
hx : mixedEmbedding.norm x ≠ 0
⊢ logMap ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * x) = (logEmbedding K) (Additive.ofMul u) + logMap 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
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) (ζ • x)) - Real.log (mixedEmbedding.norm (ζ • x)) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
unitSMul_smul,

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

Goal state before:
pp: case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ¬mixedEmbedding.norm (ζ • x) = 0

Tactic:
unitSMul_smul,

Goal state after:
case right
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
⊢ ¬mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ) * x) = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ (logEmbedding K) (Additive.ofMul u) ∈ Submodule.span ℤ (Set.range ⇑B)

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ?refine_1⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

Tactic:
· rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨(logEmbedding K) (Additive.ofMul u), ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B

case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
h : u • x ∈ fundamentalCone K
B : Module.Basis (Fin (rank K)) ℝ (logSpace K) := Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)
⊢ ⟨0, ⋯⟩ +ᵥ logMap x ∈ ZSpan.fundamentalDomain B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) = u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) =
    (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (complexConj K) ((algebraMap (𝓞 K) K) ↑u) = (algebraMap (𝓞 K) K) ↑u ↔
    ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u

Tactic:
RingOfIntegers.complexConj_eq_self_iff,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑↑u) ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) K) ↑v = (algebraMap (𝓞 K) K) ↑u
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ u • (mixedEmbedding K) ↑↑x * (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x

Tactic:
unitSMul_smul,

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ↑↑x *
      (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x
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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ (Units.complexEmbedding φ) ↑ζ ∈ rootsOfUnity (torsionOrder K) ℂ

Tactic:
exact map_complexEmbedding_torsion K φ ▸ Subgroup.apply_coe_mem_map _ _ _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑ζ • ↑a = ↑a
⊢ ζ = 1

Tactic:
unitSMul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑ζ) * ↑a = ↑a
⊢ ζ = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, ∃ (_ : a ∈ ↑↑J), (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
FractionalIdeal.mem_coeIdeal,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, ∃ (_ : ∃ x' ∈ ↑J, (algebraMap (𝓞 K) K) x' = a), (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ x ∈ idealSet K J ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑↑J, (mixedEmbedding K) ↑a = x

Tactic:
by
  simp_rw [idealSet, Set.mem_inter_iff, idealLattice, SetLike.mem_coe, FractionalIdeal.coe_mk0,
    LinearMap.mem_range, LinearMap.coe_comp, LinearMap.coe_restrictScalars, coe_subtype,
    Function.comp_apply, AlgHom.toLinearMap_apply, RingHom.toIntAlgHom_coe, Subtype.exists,
    FractionalIdeal.mem_coe, FractionalIdeal.mem_coeIdeal, exists_prop', nonempty_prop,
    exists_exists_and_eq_and]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑↑J }
⊢ ↑((idealSetEquiv K J).symm a) = ↑↑a

Tactic:
by
  rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]

Goal state after: