mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hl : w.embedding.comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver w.embedding v.embedding
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    ((ringEquivComplexOfIsComplex ⋯).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    (((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
hr : (conjugate w.embedding).comp (algebraMap K L) = v.embedding
this✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
this : ComplexEmbedding.LiesOver (conjugate (extensionEmbedding w)) (extensionEmbedding v)
x✝ : v.Completion
⊢ ((algebraMap ℂ ℂ).comp (ringEquivComplexOfIsComplex hv).toRingHom) x✝ =
    (((ringEquivComplexOfIsComplex ⋯).trans starRingAut).toRingHom.comp (algebraMap v.Completion w.Completion)) x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² ↑x✝ + x✝¹ ↑x✝ - ↑(↑x✝).mult * (∑ x, x✝² x + ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹ =
    x✝² ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝² x) * (↑(finrank ℚ K))⁻¹ +
      (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹)

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² ↑x✝ + x✝¹ ↑x✝ - ↑(↑x✝).mult * (∑ x, x✝² x + ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹ =
    x✝² ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝² x) * (↑(finrank ℚ K))⁻¹ +
      (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² * x✝¹ ↑x✝ - ↑(↑x✝).mult * (x✝² * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹ =
    x✝² * (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹)

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² * x✝¹ ↑x✝ - ↑(↑x✝).mult * (x✝² * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹ =
    x✝² * (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x✝ : v.Completion
⊢ ((((algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion =
    ((((RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
x✝ : v.Completion
⊢ ((((algebraMap v.Completion w.Completion).comp (RingEquiv.quotientBot v.Completion).toRingHom).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion =
    ((((RingEquiv.quotientBot w.Completion).toRingHom.comp (algebraMap (v.Completion ⧸ ⊥) (w.Completion ⧸ ⊥))).comp
          (Ideal.Quotient.mk ⊥))
        x✝).toCompletion
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : x ∈ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
⊢ ∑ w, x w = 0

Tactic:
induction hx using Submodule.span_induction with

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ((algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)) x✝

Tactic:
;

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ((algebraMap F K).comp (algebraMap F K).rangeRestrictFieldEquiv.symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(algebraMap F K).fieldRange) K)) x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ↑x✝ = (algebraMap (↥(algebraMap F K).fieldRange) K) x✝

Tactic:
;

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ↑x✝ = (algebraMap (↥(algebraMap F K).fieldRange) K) x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x✝ : ↥(maximalRealSubfield K)
⊢ ((algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)) x✝

Tactic:
;

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x✝ : ↥(maximalRealSubfield K)
⊢ ((algebraMap F K).comp (CMExtension.equivMaximalRealSubfield F K).symm.toRingHom) x✝ =
    ((RingEquiv.refl K).toRingHom.comp (algebraMap (↥(maximalRealSubfield K)) K)) x✝
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
x✝ : ℚ
⊢ (φ.comp (algebraMap ℚ K)) x✝ = (ψ.comp (algebraMap ℚ K)) x✝

Tactic:
;

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
x✝ : ℚ
⊢ (φ.comp (algebraMap ℚ K)) x✝ = (ψ.comp (algebraMap ℚ K)) x✝
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
x✝ : Ideal (𝓞 K)
⊢ x✝ ∈ (span {↑p}).primesOver (𝓞 K) ↔ x✝ ∈ {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
x✝ : Ideal (𝓞 K)
⊢ x✝ ∈ (span {↑p}).primesOver (𝓞 K) ↔ x✝ ∈ {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
x✝ : ℤ
⊢ (((algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
            (Int.quotientSpanNatEquivZMod p).toRingHom).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝ =
    (((RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
x✝ : ℤ
⊢ (((algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
            (Int.quotientSpanNatEquivZMod p).toRingHom).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝ =
    (((RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))).comp
        (Ideal.Quotient.mk (span {↑p})))
      x✝
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
S : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) S ∈ monicFactorsMod θ p
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) S, hQ⟩)).inertiaDeg ℤ =
    (Polynomial.map (Int.castRingHom (ZMod p)) S).natDegree

Tactic:
inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply

Goal state after:
K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
S : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) S ∈ monicFactorsMod θ p
⊢ (Polynomial.map (Int.castRingHom (ZMod p)) S).natDegree = (Polynomial.map (Int.castRingHom (ZMod p)) S).natDegree
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)ˣ
⊢ regOfFamily u / regulator K = ↑(Subgroup.closure (Set.range u) ⊔ torsion K).index

Tactic:
rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_div_regOfFamily (isMaxRank_fundSystem K)
    (by simp only [closure_fundSystem_sup_torsion_eq_top, le_top]),
    closure_fundSystem_sup_torsion_eq_top, Subgroup.relIndex_top_right]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in paramSet K,
          ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
            ∏ w, ENNReal.ofReal (↑expMapBasis x ↑w)) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
simp_rw [ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
        ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K)))) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁵ : IsDomain 𝒪
this✝⁴ : IsDedekindDomain 𝒪
this✝³ : IsFractionRing 𝒪 K
this✝² : Module.Finite ℤ 𝒪
this✝¹ : CharZero 𝒪
this✝ : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
⊢ (Ideal.under ℤ P).IsPrime

Tactic:
;

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁵ : IsDomain 𝒪
this✝⁴ : IsDedekindDomain 𝒪
this✝³ : IsFractionRing 𝒪 K
this✝² : Module.Finite ℤ 𝒪
this✝¹ : CharZero 𝒪
this✝ : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
⊢ (Ideal.under ℤ P).IsPrime
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
x✝ : mixedSpace K
⊢ x✝ ∈ {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} ↔ x✝ ∈ normLeOne K

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
x✝ : mixedSpace K
⊢ x✝ ∈ {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} ↔ x✝ ∈ normLeOne K
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ‖∑ x ∈ s, (canonicalEmbedding K) (α x)‖ ≤ ∑ i ∈ s, ‖(canonicalEmbedding K) (α i)‖

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ‖∑ x ∈ s, (canonicalEmbedding K) (α x)‖ ≤ ∑ i ∈ s, ‖(canonicalEmbedding K) (α i)‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ∀ b ∈ s, ‖(canonicalEmbedding K) (α b)‖ ≤ ‖(canonicalEmbedding K) (α b)‖

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
⊢ ∀ b ∈ s, ‖(canonicalEmbedding K) (α b)‖ ≤ ‖(canonicalEmbedding K) (α b)‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
b✝ : ι
a✝ : b✝ ∈ s
⊢ ‖(canonicalEmbedding K) (α b✝)‖ ≤ ‖(canonicalEmbedding K) (α b✝)‖

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
b✝ : ι
a✝ : b✝ ∈ s
⊢ ‖(canonicalEmbedding K) (α b✝)‖ ≤ ‖(canonicalEmbedding K) (α b✝)‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α + (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ + ‖(canonicalEmbedding K) β‖

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α + (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ + ‖(canonicalEmbedding K) β‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case h1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
τ : K →ₐ[ℚ] ℂ
a✝ : τ ∈ univ.erase σ'
⊢ ‖τ α‖ ≤ house α

Tactic:
;

Goal state after:
case h1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
τ : K →ₐ[ℚ] ℂ
a✝ : τ ∈ univ.erase σ'
⊢ ‖τ α‖ ≤ house α
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
⊢ ¬∀ (x : α × (K →+* ℂ)), (fun l ↦ ((newBasis K).repr (a x.1 l.1 * (newBasis K) l.2)) x.2) = 0 x

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
⊢ ¬∀ (x : α × (K →+* ℂ)), (fun l ↦ ((newBasis K).repr (a x.1 l.1 * (newBasis K) l.2)) x.2) = 0 x
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
⊢ ∀ (i : α) (j : β), a i j = 0 i j

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
hs : ∀ (a_1 : α) (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a a_1 l.1 * (newBasis K) l.2)) b) = 0 (a_1, b)
⊢ ∀ (i : α) (j : β), a i j = 0 i j
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ (a *ᵥ ξ K x) k = 0 k

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ (a *ᵥ ξ K x) k = 0 k
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ (a *ᵥ ξ K x) k = 0

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ (a *ᵥ ξ K x) k = 0
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
u : K →+* ℂ
| (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
u : K →+* ℂ
| (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
⊢ ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1 =
    ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
;

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
⊢ ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1 =
    ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
⊢ (fun y ↦ ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1) = fun r ↦
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
;

Goal state after:
case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
⊢ (fun y ↦ ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1) = fun r ↦
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u