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

Goal state before:
pp: k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k)

Tactic:
· rw [Nat.card_eq_fintype_card,
        ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w,
        ← Nat.card_eq_fintype_card (α := Stab w), card_stabilizer, if_pos,
        mul_one, Set.toFinset_card]
      rwa [← isUnramifiedIn_comap]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
Equiv.prodComm_symm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
              ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)) ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)))
            c (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)) ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)))
              c (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0
              ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix
                ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)) ⇑(Equiv.prodComm { w // w.IsComplex } (Fin 2)))
              c (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT K f
⊢ a ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT K f
⊢ ¬a = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT' K f w₀
⊢ a ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT' K f w₀
⊢ ¬a = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : { w // w.IsComplex } × Fin 2
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inr c)) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inr c) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr c) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inr c) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
rcases c with ⟨w, j⟩
    fin_cases j
    · simp only [Fin.zero_eta, Fin.isValue, stdBasis_apply_isComplex_fst, re_eq_add_conj,
        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
        cons_val', cons_val_zero, empty_val', cons_val_fin_one, ite_mul, cons_val_one,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      ring
    · simp only [Fin.mk_one, Fin.isValue, stdBasis_apply_isComplex_snd, im_eq_sub_conj,
        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
        cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, ite_mul, neg_mul,
        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
      ring_nf; simp [field]

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

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hr : (mk (w.embedding.comp (algebraMap K L))).embedding = conjugate (w.embedding.comp (algebraMap K L))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ (conjugate w.embedding).comp (algebraMap K L) = v.embedding

Tactic:
simpa using

Goal state after:
case inr
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hr : (mk (w.embedding.comp (algebraMap K L))).embedding = conjugate (w.embedding.comp (algebraMap K L))
⊢ w.embedding.comp (algebraMap K L) = v.embedding ∨ conjugate (w.embedding.comp (algebraMap K L)) = v.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective fun r ↦ r • 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Injective fun r ↦ ↑r
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : IsUnramified K w
hv : v.IsReal
⊢ ¬(w.comap (algebraMap K L)).IsComplex

Tactic:
simpa using

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : IsUnramified K w
hv : v.IsReal
⊢ v.IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inl
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ mixedEmbeddingsOver L v.embedding
hl : (mk ψ).embedding = ψ
⊢ ψ ∈ Sum.elim embedding (conjugate ∘ embedding) '' Set.sumEquiv.symm (ramifiedPlacesOver L v, ramifiedPlacesOver L v)

Tactic:
simpa using

Goal state after:
case inl
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ mixedEmbeddingsOver L v.embedding
hl : (mk ψ).embedding = ψ
⊢ (∃ a ∈ ramifiedPlacesOver L v, a.embedding = ψ) ∨ ∃ b ∈ ramifiedPlacesOver L v, conjugate b.embedding = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ mixedEmbeddingsOver L v.embedding
hr : (mk ψ).embedding = conjugate ψ
⊢ ψ ∈ Sum.elim embedding (conjugate ∘ embedding) '' Set.sumEquiv.symm (ramifiedPlacesOver L v, ramifiedPlacesOver L v)

Tactic:
simpa using

Goal state after:
case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ mixedEmbeddingsOver L v.embedding
hr : (mk ψ).embedding = conjugate ψ
⊢ (∃ a ∈ ramifiedPlacesOver L v, a.embedding = ψ) ∨ ∃ b ∈ ramifiedPlacesOver L v, conjugate b.embedding = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left✝ : w.LiesOver v
hw : IsUnramified K w
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w ∈ unmixedEmbeddingsOver L v.embedding

Tactic:
simpa using

Goal state after:
case pos
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left✝ : w.LiesOver v
hw : IsUnramified K w
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ w.embedding ∈ unmixedEmbeddingsOver L v.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left✝ : w.LiesOver v
hw : IsUnramified K w
h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w ∈ unmixedEmbeddingsOver L v.embedding

Tactic:
simpa using

Goal state after:
case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
left✝ : w.LiesOver v
hw : IsUnramified K w
h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ conjugate w.embedding ∈ unmixedEmbeddingsOver L v.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ :
  |((↑⟨w₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_ne : w ≠ ↑⟨w₀, hw₀⟩
⊢ w ↑a < 1

Tactic:
convert! if_neg h_ne ▸ h_le w h_ne

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

Goal state before:
pp: case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ v.embeddingConjugateIte (mk ψ) = ψ

Tactic:
simpa using

Goal state after:
case inr
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
ψ : L →+* ℂ
h : ψ ∈ unmixedEmbeddingsOver L v.embedding
hψ : (mk ψ).embedding = conjugate ψ
⊢ ComplexEmbedding.LiesOver (conjugate ψ) v.embedding → conjugate ψ = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
σ : L →ₐ[K] ℂ
x✝ : σ ∈ ↑univ
⊢ σ.toRingHom ∈ ↑⋯.toFinset

Tactic:
simpa using

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
σ : L →ₐ[K] ℂ
x✝ : σ ∈ ↑univ
⊢ ComplexEmbedding.LiesOver (↑σ) v.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (euclidean.integerLattice K)

Tactic:
simp_rw [euclidean.integerLattice]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsZLattice ℝ (ZLattice.comap ℝ (mixedEmbedding.integerLattice K) ↑↑(toMixed K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ a ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ¬a = 0
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
inst✝²¹ : Field L₃
inst✝²⁰ : Algebra A K
inst✝¹⁹ : IsFractionRing A K
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : Algebra A L
inst✝¹⁶ : IsScalarTower A K L
inst✝¹⁵ : Algebra K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
inst✝¹² : Algebra K L₃
inst✝¹¹ : Algebra A L₃
inst✝¹⁰ : IsScalarTower A K L₃
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : IsIntegralClosure B₃ A L₃
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝¹ : IsDomain A
this✝ : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : A
hx : x ∈ ↑A⁰
⊢ IsUnit (((algebraMap B₂ L₂).comp ↑σ) ↑⟨(algebraMap A B) x, ⋯⟩)

Tactic:
simpa using

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝³¹ : CommRing A
inst✝³⁰ : CommRing B
inst✝²⁹ : CommRing B₂
inst✝²⁸ : CommRing B₃
inst✝²⁷ : Algebra A B
inst✝²⁶ : Algebra A B₂
inst✝²⁵ : Algebra A B₃
inst✝²⁴ : Field K
inst✝²³ : Field L
inst✝²² : Field L₂
inst✝²¹ : Field L₃
inst✝²⁰ : Algebra A K
inst✝¹⁹ : IsFractionRing A K
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : Algebra A L
inst✝¹⁶ : IsScalarTower A K L
inst✝¹⁵ : Algebra K L₂
inst✝¹⁴ : Algebra A L₂
inst✝¹³ : IsScalarTower A K L₂
inst✝¹² : Algebra K L₃
inst✝¹¹ : Algebra A L₃
inst✝¹⁰ : IsScalarTower A K L₃
inst✝⁹ : Algebra B L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : Algebra B₂ L₂
inst✝⁵ : IsScalarTower A B₂ L₂
inst✝⁴ : IsIntegralClosure B₂ A L₂
inst✝³ : Algebra B₃ L₃
inst✝² : IsScalarTower A B₃ L₃
inst✝¹ : IsIntegralClosure B₃ A L₃
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this✝¹ : IsDomain A
this✝ : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : A
hx : x ∈ ↑A⁰
⊢ ¬x = 0
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : ∀ (g : Gal(L/K)), g • b = b
⊢ (algebraMap B L) b ∈ IntermediateField.fixedField ⊤

Tactic:
rintro ⟨g, -⟩

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : ∀ (g : Gal(L/K)), g • b = b
g : Gal(L/K)
property✝ : g ∈ ⊤
⊢ ⟨g, property✝⟩ • (algebraMap B L) b = (algebraMap B L) b
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝⁴² : CommRing A
inst✝⁴¹ : CommRing B
inst✝⁴⁰ : CommRing B₂
inst✝³⁹ : CommRing B₃
inst✝³⁸ : Algebra A B
inst✝³⁷ : Algebra A B₂
inst✝³⁶ : Algebra A B₃
inst✝³⁵ : Field K
inst✝³⁴ : Field L
inst✝³³ : Field L₂
inst✝³² : Field L₃
inst✝³¹ : Algebra A K
inst✝³⁰ : IsFractionRing A K
inst✝²⁹ : Algebra K L
inst✝²⁸ : Algebra A L
inst✝²⁷ : IsScalarTower A K L
inst✝²⁶ : Algebra K L₂
inst✝²⁵ : Algebra A L₂
inst✝²⁴ : IsScalarTower A K L₂
inst✝²³ : Algebra K L₃
inst✝²² : Algebra A L₃
inst✝²¹ : IsScalarTower A K L₃
inst✝²⁰ : Algebra B L
inst✝¹⁹ : IsScalarTower A B L
inst✝¹⁸ : IsIntegralClosure B A L
inst✝¹⁷ : Algebra B₂ L₂
inst✝¹⁶ : IsScalarTower A B₂ L₂
inst✝¹⁵ : IsIntegralClosure B₂ A L₂
inst✝¹⁴ : Algebra B₃ L₃
inst✝¹³ : IsScalarTower A B₃ L₃
inst✝¹² : IsIntegralClosure B₃ A L₃
inst✝¹¹ : FiniteDimensional K L
Aₘ : Type ?u.109
Bₘ : Type ?u.111
inst✝¹⁰ : CommRing Aₘ
inst✝⁹ : CommRing Bₘ
inst✝⁸ : Algebra Aₘ Bₘ
inst✝⁷ : Algebra A Aₘ
inst✝⁶ : Algebra B Bₘ
inst✝⁵ : Algebra A Bₘ
inst✝⁴ : IsScalarTower A Aₘ Bₘ
inst✝³ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝² : IsLocalization M Aₘ
inst✝¹ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝ : IsIntegrallyClosed A
x y : B
⊢ IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) (x * y))) ⋯ =
    IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x)) ⋯ *
      IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) y)) ⋯

Tactic:
simpa using

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst✝⁴² : CommRing A
inst✝⁴¹ : CommRing B
inst✝⁴⁰ : CommRing B₂
inst✝³⁹ : CommRing B₃
inst✝³⁸ : Algebra A B
inst✝³⁷ : Algebra A B₂
inst✝³⁶ : Algebra A B₃
inst✝³⁵ : Field K
inst✝³⁴ : Field L
inst✝³³ : Field L₂
inst✝³² : Field L₃
inst✝³¹ : Algebra A K
inst✝³⁰ : IsFractionRing A K
inst✝²⁹ : Algebra K L
inst✝²⁸ : Algebra A L
inst✝²⁷ : IsScalarTower A K L
inst✝²⁶ : Algebra K L₂
inst✝²⁵ : Algebra A L₂
inst✝²⁴ : IsScalarTower A K L₂
inst✝²³ : Algebra K L₃
inst✝²² : Algebra A L₃
inst✝²¹ : IsScalarTower A K L₃
inst✝²⁰ : Algebra B L
inst✝¹⁹ : IsScalarTower A B L
inst✝¹⁸ : IsIntegralClosure B A L
inst✝¹⁷ : Algebra B₂ L₂
inst✝¹⁶ : IsScalarTower A B₂ L₂
inst✝¹⁵ : IsIntegralClosure B₂ A L₂
inst✝¹⁴ : Algebra B₃ L₃
inst✝¹³ : IsScalarTower A B₃ L₃
inst✝¹² : IsIntegralClosure B₃ A L₃
inst✝¹¹ : FiniteDimensional K L
Aₘ : Type ?u.109
Bₘ : Type ?u.111
inst✝¹⁰ : CommRing Aₘ
inst✝⁹ : CommRing Bₘ
inst✝⁸ : Algebra Aₘ Bₘ
inst✝⁷ : Algebra A Aₘ
inst✝⁶ : Algebra B Bₘ
inst✝⁵ : Algebra A Bₘ
inst✝⁴ : IsScalarTower A Aₘ Bₘ
inst✝³ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝² : IsLocalization M Aₘ
inst✝¹ : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝ : IsIntegrallyClosed A
x y : B
⊢ IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x) * (norm K) ((algebraMap B L) y)) ⋯ =
    IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) x)) ⋯ *
      IsIntegralClosure.mk' A ((norm K) ((algebraMap B L) y)) ⋯
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
A : AffineSubspace ℝ (realSpace K) := ↑{ carrier := {x | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
h : A = ⊤
⊢ False

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
A : AffineSubspace ℝ (realSpace K) := ↑{ carrier := {x | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
h : A = ⊤
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsComplex }
⊢ normAtComplexPlaces x ↑w = ‖x.2 w‖

Tactic:
by
  rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]

Goal state after: