-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem toDerivation_injective :
    Function.Injective (toDerivation : LeftInvariantDerivation I G → _) :=
  fun X Y h => by cases X; cases Y; congr

Proof state:
case mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
Y : LeftInvariantDerivation I G
toDerivation✝ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝) = (Derivation.evalAt g) toDerivation✝
h : ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = ↑Y
⊢ { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = Y

Tactic:
cases Y

Result:
case mk.mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
toDerivation✝¹ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝¹ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝¹) = (Derivation.evalAt g) toDerivation✝¹
toDerivation✝ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝) = (Derivation.evalAt g) toDerivation✝
h :
  ↑{ toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
⊢ { toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
X Y : LeftInvariantDerivation I G
h : ↑X = ↑Y
⊢ X = Y

Tactic:
cases X

Result:
case mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
Y : LeftInvariantDerivation I G
toDerivation✝ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝) = (Derivation.evalAt g) toDerivation✝
h : ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = ↑Y
⊢ { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ } = Y

Proof state:
case mk.mk
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
toDerivation✝¹ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝¹ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝¹) = (Derivation.evalAt g) toDerivation✝¹
toDerivation✝ : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''✝ : ∀ (g : G), (𝒅ₕ ⋯) ((Derivation.evalAt 1) toDerivation✝) = (Derivation.evalAt g) toDerivation✝
h :
  ↑{ toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    ↑{ toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }
⊢ { toDerivation := toDerivation✝¹, left_invariant'' := left_invariant''✝¹ } =
    { toDerivation := toDerivation✝, left_invariant'' := left_invariant''✝ }

Tactic:
congr

Result:
no goals