-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem coeFn_injective : Function.Injective ((↑) : ENormedSpace 𝕜 V → V → ℝ≥0∞)

Proof state:
case mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e₂ : ENormedSpace 𝕜 V
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h : ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = ↑e₂
⊢ { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = e₂

Tactic:
cases e₂

Result:
case mk.mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
toFun✝¹ : V → ℝ≥0∞
eq_zero'✝¹ : ∀ (x : V), toFun✝¹ x = 0 → x = 0
map_add_le'✝¹ : ∀ (x y : V), toFun✝¹ (x + y) ≤ toFun✝¹ x + toFun✝¹ y
map_smul_le'✝¹ : ∀ (c : 𝕜) (x : V), toFun✝¹ (c • x) ≤ ↑‖c‖₊ * toFun✝¹ x
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h :
  ↑{ toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
⊢ { toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
⊢ Function.Injective toFun

Tactic:
intro e₁ e₂ h

Result:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e₁ e₂ : ENormedSpace 𝕜 V
h : ↑e₁ = ↑e₂
⊢ e₁ = e₂

Proof state:
case mk.mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
toFun✝¹ : V → ℝ≥0∞
eq_zero'✝¹ : ∀ (x : V), toFun✝¹ x = 0 → x = 0
map_add_le'✝¹ : ∀ (x y : V), toFun✝¹ (x + y) ≤ toFun✝¹ x + toFun✝¹ y
map_smul_le'✝¹ : ∀ (c : 𝕜) (x : V), toFun✝¹ (c • x) ≤ ↑‖c‖₊ * toFun✝¹ x
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h :
  ↑{ toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
⊢ { toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }

Tactic:
congr

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e₁ e₂ : ENormedSpace 𝕜 V
h : ↑e₁ = ↑e₂
⊢ e₁ = e₂

Tactic:
cases e₁

Result:
case mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e₂ : ENormedSpace 𝕜 V
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h : ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = ↑e₂
⊢ { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = e₂