-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mem_span_fractionalIdealLatticeBasis {x : (mixedSpace K)} :
    x ∈ Submodule.span ℤ (Set.range (fractionalIdealLatticeBasis K I)) ↔
      x ∈ mixedEmbedding K '' I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Set.range ⇑(fractionalIdealLatticeBasis K I) =
    ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(basisOfFractionalIdeal K I)

Tactic:
rw [← Set.range_comp]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Set.range ⇑(fractionalIdealLatticeBasis K I) =
    Set.range (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(basisOfFractionalIdeal K I))

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rw [show Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) = (I : Set K) by
      ext; erw [mem_span_basisOfFractionalIdeal]]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑↑I ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑↑I ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ Set.range ⇑(fractionalIdealLatticeBasis K I) =
    Set.range (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(basisOfFractionalIdeal K I))

Tactic:
exact congr_arg Set.range (funext (fun i ↦ fractionalIdealLatticeBasis_apply K I i))

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) = ↑↑I

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
x✝ : K
⊢ x✝ ∈ ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔ x✝ ∈ ↑↑I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rw [show Set.range (fractionalIdealLatticeBasis K I) =
      (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (basisOfFractionalIdeal K I)) by
    rw [← Set.range_comp]
    exact congr_arg Set.range (funext (fun i ↦ fractionalIdealLatticeBasis_apply K I i))]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(basisOfFractionalIdeal K I)) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(basisOfFractionalIdeal K I)) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ ⇑(mixedEmbedding K).toIntAlgHom.toLinearMap '' ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔
    x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
x✝ : K
⊢ x✝ ∈ ↑(Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I))) ↔ x✝ ∈ ↑↑I

Tactic:
erw [mem_span_basisOfFractionalIdeal]

Result:
no goals