-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem coe_injective : @Function.Injective (VectorMeasure α M) (Set α → M) (⇑) := fun v w h => by
  cases v
  cases w
  congr

Proof state:
case mk
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
w : VectorMeasure α M
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ i, f i))
h : ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = ↑w
⊢ { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = w

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
measureOf'✝¹ : Set α → M
empty'✝¹ : measureOf'✝¹ ∅ = 0
not_measurable'✝¹ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝¹ i = 0
m_iUnion'✝¹ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝¹ (f i)) (measureOf'✝¹ (⋃ i, f i))
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ i, f i))
h :
  ↑{ measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }
⊢ { measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }

Proof state:
case mk.mk
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
measureOf'✝¹ : Set α → M
empty'✝¹ : measureOf'✝¹ ∅ = 0
not_measurable'✝¹ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝¹ i = 0
m_iUnion'✝¹ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝¹ (f i)) (measureOf'✝¹ (⋃ i, f i))
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ i, f i))
h :
  ↑{ measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }
⊢ { measureOf' := measureOf'✝¹, empty' := empty'✝¹, not_measurable' := not_measurable'✝¹, m_iUnion' := m_iUnion'✝¹ } =
    { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ }

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ↑v = ↑w
⊢ v = w

Tactic:
cases v

Result:
case mk
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
w : VectorMeasure α M
measureOf'✝ : Set α → M
empty'✝ : measureOf'✝ ∅ = 0
not_measurable'✝ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → measureOf'✝ i = 0
m_iUnion'✝ :
  ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Disjoint on f) → HasSum (fun i => measureOf'✝ (f i)) (measureOf'✝ (⋃ i, f i))
h : ↑{ measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = ↑w
⊢ { measureOf' := measureOf'✝, empty' := empty'✝, not_measurable' := not_measurable'✝, m_iUnion' := m_iUnion'✝ } = w