-- Mathlib/Algebra/Lie/Basic.lean
theorem coe_injective : @Function.Injective (M →ₗ⁅R,L⁆ N) (M → N) (↑)

Proof state:
case mk.mk.mk.mk.mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M → N
map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆
g : M → N
map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆
h :
  ⇑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    ⇑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
⊢ Injective DFunLike.coe

Tactic:
rintro ⟨⟨⟨f, _⟩⟩⟩ ⟨⟨⟨g, _⟩⟩⟩ h

Result:
case mk.mk.mk.mk.mk.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M → N
map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆
g : M → N
map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆
h :
  ⇑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    ⇑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }