-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem conj_apply {x : ((K →+* ℂ) → ℂ)} (φ : K →+* ℂ)
    (hx : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K))) :
    conj (x φ) = x (ComplexEmbedding.conjugate φ)

Proof state:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]

Result:
no goals

Proof state:
case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.zero_apply, Pi.zero_apply, map_zero]

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ ∀ x ∈ Set.range ⇑(canonicalEmbedding K), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case refine_1.intro
K : Type u_1
inst✝ : Field K
x✝ : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x✝ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x : K
⊢ (starRingEnd ℂ) ((canonicalEmbedding K) x φ) = (canonicalEmbedding K) x (ComplexEmbedding.conjugate φ)

Proof state:
case refine_1.intro
K : Type u_1
inst✝ : Field K
x✝ : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x✝ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x : K
⊢ (starRingEnd ℂ) ((canonicalEmbedding K) x φ) = (canonicalEmbedding K) x (ComplexEmbedding.conjugate φ)

Tactic:
rw [apply_at, apply_at, ComplexEmbedding.conjugate_coe_eq]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

Tactic:
refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx

Result:
case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ ∀ x ∈ Set.range ⇑(canonicalEmbedding K), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)

case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Proof state:
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
rw [Pi.smul_apply, Complex.real_smul, map_mul, Complex.conj_ofReal]

Result:
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ ↑a * (starRingEnd ℂ) (x✝¹ φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)