-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem gelfandTransform_bijective : Function.Bijective (gelfandTransform ℂ A)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
⊢ rng = ⊤

Tactic:
refine h ▸ ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints
  _ (fun _ _ => ?_)

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ x✝¹ ≠ x✝ → ∃ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ ≠ f x✝

Proof state:
case h.h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
φ : ↑(characterSpace ℂ A)
⊢ ((gelfandTransform ℂ A).toRingHom (star a)) φ = (star ((gelfandTransform ℂ A).toRingHom a)) φ

Tactic:
dsimp

Result:
case h.h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
φ : ↑(characterSpace ℂ A)
⊢ φ (star a) = (starRingEnd ℂ) (φ a)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ Function.Surjective ⇑(gelfandTransform ℂ A)

Tactic:
let rng : StarSubalgebra ℂ C(characterSpace ℂ A, ℂ) :=
  { toSubalgebra := (gelfandTransform ℂ A).range
    star_mem' := by
      rintro - ⟨a, rfl⟩
      use star a
      ext1 φ
      dsimp
      simp only [map_star, RCLike.star_def] }

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
⊢ Function.Surjective ⇑(gelfandTransform ℂ A)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
⊢ Function.Surjective ⇑(gelfandTransform ℂ A)

Tactic:
suffices rng = ⊤ from
  fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
⊢ rng = ⊤

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ Function.Bijective ⇑(gelfandTransform ℂ A)

Tactic:
refine ⟨(gelfandTransform_isometry A).injective, ?_⟩

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ Function.Surjective ⇑(gelfandTransform ℂ A)

Proof state:
case h.h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
φ : ↑(characterSpace ℂ A)
⊢ φ (star a) = (starRingEnd ℂ) (φ a)

Tactic:
simp only [map_star, RCLike.star_def]

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
    a ∈ (gelfandTransform ℂ A).range.carrier → star a ∈ (gelfandTransform ℂ A).range.carrier

Tactic:
rintro - ⟨a, rfl⟩

Result:
case intro
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ star ((gelfandTransform ℂ A).toRingHom a) ∈ (gelfandTransform ℂ A).range.carrier

Proof state:
case h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ (gelfandTransform ℂ A).toRingHom (star a) = star ((gelfandTransform ℂ A).toRingHom a)

Tactic:
ext1 φ

Result:
case h.h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
φ : ↑(characterSpace ℂ A)
⊢ ((gelfandTransform ℂ A).toRingHom (star a)) φ = (star ((gelfandTransform ℂ A).toRingHom a)) φ

Proof state:
case intro
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ star ((gelfandTransform ℂ A).toRingHom a) ∈ (gelfandTransform ℂ A).range.carrier

Tactic:
use star a

Result:
case h
A : Type u_1
inst✝ : CommCStarAlgebra A
a : A
⊢ (gelfandTransform ℂ A).toRingHom (star a) = star ((gelfandTransform ℂ A).toRingHom a)

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
⊢ rng = ⊤

Tactic:
have h : rng.topologicalClosure = rng := le_antisymm
  (StarSubalgebra.topologicalClosure_minimal le_rfl
    (gelfandTransform_isometry A).isClosedEmbedding.isClosed_range)
  (StarSubalgebra.le_topologicalClosure _)

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
⊢ rng = ⊤

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ (∀ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ = f x✝) → x✝¹ = x✝

Tactic:
exact fun h => Subtype.ext (ContinuousLinearMap.ext fun a =>
  h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ x✝¹ ≠ x✝ → ∃ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ ≠ f x✝

Tactic:
contrapose!

Result:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) := { toSubalgebra := (gelfandTransform ℂ A).range, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ (∀ f ∈ (fun f => ⇑f) '' ↑rng.toSubalgebra, f x✝¹ = f x✝) → x✝¹ = x✝