-- Mathlib/Probability/Moments/ComplexMGF.lean
/-- If two random variables have the same moment generating function then they have
the same `integrableExpSet`. -/
lemma integrableExpSet_eq_of_mgf' (hXY : mgf X μ = mgf Y μ') (hμμ' : μ = 0 ↔ μ' = 0) :
    integrableExpSet X μ = integrableExpSet Y μ'

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
ext t

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
⊢ t ∈ integrableExpSet X μ ↔ t ∈ integrableExpSet Y μ'

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : μ = 0
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Tactic:
simp [hμ, hμμ'.mp hμ]

Result:
no goals

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
⊢ t ∈ integrableExpSet X μ ↔ t ∈ integrableExpSet Y μ'

Tactic:
simp only [integrableExpSet, Set.mem_setOf_eq]

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this✝ : NeZero μ
this : NeZero μ'
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Tactic:
rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]

Result:
no goals

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Tactic:
by_cases hμ : μ = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : μ = 0
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this : NeZero μ
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Tactic:
have : NeZero μ' := ⟨(not_iff_not.mpr hμμ').mp hμ⟩

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this✝ : NeZero μ
this : NeZero μ'
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'

Tactic:
have : NeZero μ := ⟨hμ⟩

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this : NeZero μ
⊢ Integrable (fun ω => rexp (t * X ω)) μ ↔ Integrable (fun ω => rexp (t * Y ω)) μ'