induction x
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
x y : Distribution X
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪x, φ⟫ = ⟪y, φ⟫) →
    x = y
case mk
W : Type ?u.14465
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type ?u.14918
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.15144
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
y : Distribution X
action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
⊢ (∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
      ⟪{ action := action✝ }, φ⟫ = ⟪y, φ⟫) →
    { action := action✝ } = y