-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem coe_injective : Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂)

Proof state:
case mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝, cont := cont✝ } = ↑g
⊢ { toLinearMap := toLinearMap✝, cont := cont✝ } = g

Tactic:
cases g

Result:
case mk.mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
toLinearMap✝¹ : M₁ →ₛₗ[σ₁₂] M₂
cont✝¹ : Continuous toLinearMap✝¹.toFun
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = ↑{ toLinearMap := toLinearMap✝, cont := cont✝ }
⊢ { toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = { toLinearMap := toLinearMap✝, cont := cont✝ }

Proof state:
case mk.mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
toLinearMap✝¹ : M₁ →ₛₗ[σ₁₂] M₂
cont✝¹ : Continuous toLinearMap✝¹.toFun
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = ↑{ toLinearMap := toLinearMap✝, cont := cont✝ }
⊢ { toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = { toLinearMap := toLinearMap✝, cont := cont✝ }

Tactic:
congr

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
⊢ Function.Injective toLinearMap

Tactic:
intro f g H

Result:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
H : ↑f = ↑g
⊢ f = g

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
H : ↑f = ↑g
⊢ f = g

Tactic:
cases f

Result:
case mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝, cont := cont✝ } = ↑g
⊢ { toLinearMap := toLinearMap✝, cont := cont✝ } = g