Theorem: SciLean.Prob.Distribution.ext (SciLean/Modules/Prob/DistribDeriv/Distribution.lean)

State before:
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
Tactic:
induction x
State after:
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

State before:
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
Tactic:
induction y
State after:
case mk.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
action✝¹ 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✝¹ }, φ⟫ = ⟪{ action := action✝ }, φ⟫) →
    { action := action✝¹ } = { action := action✝ }

State before:
case mk.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
action✝¹ 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✝¹ }, φ⟫ = ⟪{ action := action✝ }, φ⟫) →
    { action := action✝¹ } = { action := action✝ }
Tactic:
simp only [action_mk_apply, mk.injEq]
State after:
case mk.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
action✝¹ 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✝ φ) →
    action✝¹ = action✝

State before:
case mk.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
action✝¹ 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✝ φ) →
    action✝¹ = action✝
Tactic:
intro h
State after:
case mk.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
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
⊢ action✝¹ = action✝

State before:
case mk.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
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
⊢ action✝¹ = action✝
Tactic:
funext _ _ _ _ φ
State after:
case mk.mk.h.h.h.h.h
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
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
x✝³ : Type u
x✝² : NormedAddCommGroup x✝³
x✝¹ : NormedSpace ℝ x✝³
x✝ : CompleteSpace x✝³
φ : X → x✝³
⊢ action✝¹ φ = action✝ φ

State before:
case mk.mk.h.h.h.h.h
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
action✝¹ action✝ :
  {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
h :
  ∀ {Y : Type u} [inst : NormedAddCommGroup Y] [inst_1 : NormedSpace ℝ Y] [inst_2 : CompleteSpace Y] (φ : X → Y),
    action✝¹ φ = action✝ φ
x✝³ : Type u
x✝² : NormedAddCommGroup x✝³
x✝¹ : NormedSpace ℝ x✝³
x✝ : CompleteSpace x✝³
φ : X → x✝³
⊢ action✝¹ φ = action✝ φ
Tactic:
apply (h φ)
State after:
no goals