-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem disjoint_span_commMap_ker [NumberField K] :
    Disjoint (Submodule.span ℝ (Set.range (canonicalEmbedding.latticeBasis K)))
      (LinearMap.ker (commMap K))

Proof state:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ((commMap K) x).1 ⟨InfinitePlace.mk φ, ⋯⟩ = Complex.re 0

Tactic:
exact congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ x φ = 0

Tactic:
have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩

Result:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
⊢ x φ = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))

Tactic:
refine (Submodule.span_mono ?_) h_mem

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ Set.range ⇑(canonicalEmbedding.latticeBasis K) ⊆ Set.range ⇑(canonicalEmbedding K)

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0 φ

Tactic:
rw [Pi.zero_apply]

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ x = 0

Tactic:
ext1 φ

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0 φ

Proof state:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).re = Complex.re 0

Tactic:
rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]

Result:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ((commMap K) x).1 ⟨InfinitePlace.mk φ, ⋯⟩ = Complex.re 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ Set.range ⇑(canonicalEmbedding.latticeBasis K) ⊆ Set.range ⇑(canonicalEmbedding K)

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (canonicalEmbedding.latticeBasis K) i ∈ Set.range ⇑(canonicalEmbedding K)

Proof state:
case pos.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).im = Complex.im 0

Tactic:
rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
  ComplexEmbedding.isReal_iff.mp hφ]

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (canonicalEmbedding.latticeBasis K) i ∈ Set.range ⇑(canonicalEmbedding K)

Tactic:
exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ x = 0

Tactic:
replace h_mem : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K)) := by
  refine (Submodule.span_mono ?_) h_mem
  rintro _ ⟨i, rfl⟩
  exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ x = 0

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
⊢ x φ = 0

Tactic:
cases embedding_mk_eq φ with
| inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
| inr h =>
    apply RingHom.injective (starRingEnd ℂ)
    rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
      ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

Result:
no goals

Proof state:
case neg.inr.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (starRingEnd ℂ) (x φ) = (starRingEnd ℂ) 0

Tactic:
rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
  ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

Result:
no goals

Proof state:
case neg.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : (fun x => x.2) ((commMap K) x) ⟨InfinitePlace.mk φ, ⋯⟩ = (fun x => x.2) 0 ⟨InfinitePlace.mk φ, ⋯⟩
h : (InfinitePlace.mk φ).embedding = φ
⊢ x φ = 0

Tactic:
rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Disjoint (Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))) (LinearMap.ker (commMap K))

Tactic:
refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))
h_zero : (commMap K) x = 0
⊢ x = 0