awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv 0 (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1 * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
      HasDerivAt (iteratedDeriv n (complexMGF X μ))
        (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z)
  {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
  HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
Tactic: induction n generalizing z with
  | zero => simp [hasDerivAt_complexMGF hz]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp hz (n + 1)
Cleared hypotheses: z, hz, n
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (complexMGF X μ) z =
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have succ : deriv (iteratedDeriv n (complexMGF X μ)) z =
  ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
Tactic: rw [iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have zero : ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
  iteratedDeriv 0 (complexMGF X μ) z =
    ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (z * (↑(X ω) : ℂ))) x ∂μ
Tactic: induction n generalizing z with
  | zero => simp [complexMGF]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv
Cleared hypotheses: z, hz, n
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    iteratedDeriv 0 (complexMGF X μ) z =
      ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (z * (↑(X ω) : ℂ))) x ∂μ
⊢ iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
      iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
  {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
  iteratedDeriv (n + 1) (complexMGF X μ) z =
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
Tactic: induction n generalizing z with
  | zero => simp [complexMGF]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv
Cleared hypotheses: z, hz, n
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 μ'
have h : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ t ∈ integrableExpSet Y μ'
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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 ω)) μ'
have pos : ∀ (hμ : μ = 0),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
pos :
  ∀ (hμ : μ = 0),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
have neg : ∀ (hμ : ¬μ = 0),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
Tactic: by_cases hμ : μ = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : 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 ω)) μ'
have this : NeZero μ
Tactic: have : NeZero μ := ⟨hμ⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : 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 ω)) μ'
have this₁ : NeZero μ'
Tactic: have : NeZero μ' := ⟨(not_iff_not.mpr hμμ').mp hμ⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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_1 : NeZero μ
this : NeZero μ'
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
have neg : 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
Tactic: rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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_1 : NeZero μ
this : NeZero μ'
neg : 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
have neg₁ : 0 < mgf X μ t ↔ 0 < mgf Y μ' t
Tactic: rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : 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_1 : NeZero μ
this : NeZero μ'
neg : 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
neg₁ : 0 < mgf X μ t ↔ 0 < mgf Y μ' t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
have neg₂ : 0 < mgf Y μ' t ↔ 0 < mgf Y μ' t
Tactic: rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ integrableExpSet X μ = integrableExpSet Y μ'
have refine : μ = 0 ↔ μ' = 0
Tactic: refine integrableExpSet_eq_of_mgf' hXY ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ μ = 0 ↔ μ' = 0
have simp : ¬μ' = 0
Tactic: simp only [IsProbabilityMeasure.ne_zero, false_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ ¬μ' = 0
have suffices : mgf Y μ' 0 ≠ 0
Tactic: suffices mgf Y μ' 0 ≠ 0 by
    intro h_contra
    simp [h_contra] at this
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ mgf Y μ' 0 ≠ 0
have rw : mgf X μ 0 ≠ 0
Tactic: rw [← hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have pos : ∀ (h_empty : interior (integrableExpSet X μ) = ∅),
  Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
Tactic: by_cases h_empty : interior (integrableExpSet X μ) = ∅
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
pos :
  ∀ (h_empty : interior (integrableExpSet X μ) = ∅),
    Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have neg : ∀ (h_empty : ¬interior (integrableExpSet X μ) = ∅),
  Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
Tactic: by_cases h_empty : interior (integrableExpSet X μ) = ∅
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : ¬interior (integrableExpSet X μ) = ∅
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have h_empty₁ : (interior (integrableExpSet X μ)).Nonempty
Tactic: rw [← ne_eq, ← Set.nonempty_iff_ne_empty] at h_empty
Cleared hypotheses: h_empty
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : (interior (integrableExpSet X μ)).Nonempty
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have neg : ∀ (t : ℝ) (ht : t ∈ interior (integrableExpSet X μ)),
  Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
Tactic: obtain ⟨t, ht⟩ := h_empty
Cleared hypotheses: h_empty
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
Tactic: have hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
    analyticOnNhd_complexMGF
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
Tactic: have hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')} :=
    analyticOnNhd_complexMGF
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
have neg : ∀ (ht : t ∈ interior (integrableExpSet Y μ'))
  (hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')})
  (hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}),
  Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
Tactic: rw [integrableExpSet_eq_of_mgf' hXY hμμ'] at hX ht ⊢
Cleared hypotheses: ht, hX, hY
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
have neg : ∃ᶠ (z : ℂ) in 𝓝[≠] (↑t : ℂ), complexMGF X μ z = complexMGF Y μ' z
Tactic: refine AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq hX hY
    (convex_integrableExpSet.interior.linear_preimage reLm).isPreconnected
    (z₀ := (t : ℂ)) (by simp [ht]) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)
have refine : ∀ (y : ℝ), complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)
Tactic: refine .of_forall fun y ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
y : ℝ
⊢ complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)
have rw : (↑(mgf X μ y) : ℂ) = complexMGF Y μ' (↑y : ℂ)
Tactic: rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
y : ℝ
rw : (↑(mgf X μ y) : ℂ) = complexMGF Y μ' (↑y : ℂ)
⊢ complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)
have rw₁ : (↑(mgf X μ y) : ℂ) = (↑(mgf Y μ' y) : ℂ)
Tactic: rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
y : ℝ
rw : (↑(mgf X μ y) : ℂ) = complexMGF Y μ' (↑y : ℂ)
rw₁ : (↑(mgf X μ y) : ℂ) = (↑(mgf Y μ' y) : ℂ)
⊢ complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)
have rw₂ : (↑(mgf Y μ' y) : ℂ) = (↑(mgf Y μ' y) : ℂ)
Tactic: rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] (↑t : ℂ), complexMGF X μ z = complexMGF Y μ' z
have h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)
Tactic: have h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ x = complexMGF Y μ' x := by
    refine .of_forall fun y ↦ ?_
    rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] (↑t : ℂ), complexMGF X μ z = complexMGF Y μ' z
have neg : ∀
  (h_real :
    ∃ (ns : ℕ → ℝ),
      Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ (↑(ns n) : ℂ) = complexMGF Y μ' (↑(ns n) : ℂ)),
  ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
Tactic: rw [frequently_iff_seq_forall] at h_real ⊢
Cleared hypotheses: h_real
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
h_real :
  ∃ (ns : ℕ → ℝ), Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ (↑(ns n) : ℂ) = complexMGF Y μ' (↑(ns n) : ℂ)
⊢ ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
have neg : ∀ (xs : ℕ → ℝ) (hx_tendsto : Tendsto xs atTop (𝓝[≠] t))
  (hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)),
  ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
Tactic: obtain ⟨xs, hx_tendsto, hx_eq⟩ := h_real
Cleared hypotheses: h_real
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝[≠] t)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
have neg : Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝[≠] (↑t : ℂ))
Tactic: refine ⟨fun n ↦ xs n, ?_, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝[≠] t)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝[≠] (↑t : ℂ))
have neg : ∀ (hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n))
  (hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)),
  Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ)) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
Tactic: rw [tendsto_nhdsWithin_iff] at hx_tendsto ⊢
Cleared hypotheses: hx_tendsto, hx_eq
-- Lean 4 proof step from Mathlib.Probability.Moments.ComplexMGF (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ)) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
have neg : Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ))
Tactic: constructor