Theorem: SciLean.Rand.add_as_flip_E (SciLean/Core/Rand/Distributions/Flip.lean)

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = (flip θ).𝔼 fun b => if b = true then θ⁻¹ • x else (1 - θ)⁻¹ • y
Tactic:
simp[flip.E]
State after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
have : θ ≠ 0 := by aesop
State after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
have : 1 - θ ≠ 0 := by sorry_proof
State after:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this✝ : θ ≠ 0
this : 1 - θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this✝ : θ ≠ 0
this : 1 - θ ≠ 0
⊢ x + y = θ • θ⁻¹ • x + (1 - θ) • (1 - θ)⁻¹ • y
Tactic:
simp (disch:=assumption)
State after:
no goals

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
⊢ θ ≠ 0
Tactic:
aesop
State after:
no goals

State before:
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ 1 - θ ≠ 0
Tactic:
sorry_proof
State after:
no goals