awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFunDual (mE := mE) (Measure.map (fun (ω : Ω) ↦ X ω + Y ω) P) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := mE) (Measure.map X P))
      (charFunDual (mE := mE) (Measure.map Y P))

Tactic:
hXY.charFunDual_map_add_eq_mul mX mY

Premises used: ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
mY : AEMeasurable Prod.snd (μ.prod ν)
hXY : Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
⊢ charFunDual (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) =
    HMul.hMul (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)

Tactic:
rw [IndepFun.charFunDual_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]

Premises used: ProbabilityTheory.IndepFun.charFunDual_map_fun_add_eq_mul, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_snd, MeasureTheory.measurePreserving_fst
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.fst (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ AEMeasurable Prod.snd (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
indepFun_prod (X := id) (Y := id) measurable_id measurable_id

Premises used: ProbabilityTheory.indepFun_prod, measurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : NormedSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd

Tactic:
exact indepFun_prod (X := id) (Y := id) measurable_id measurable_id

Premises used: ProbabilityTheory.indepFun_prod, measurable_id
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : NormedSpace ℝ E
inst_9 : NormedSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
rw :
  Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
      (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
rw₁ rw₂ :
  (∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))) ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (mE := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P) L =
        charFunDual (mE := mE) (Measure.map X P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
          charFunDual (mE := mF) (Measure.map Y P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]

Premises used: MeasureTheory.charFunDual_eq_prod_iff, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
inst_1 : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
mF : MeasurableSpace F
inst_5 : NormedAddCommGroup F
inst_6 : CompleteSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_9 : NormedSpace ℝ E
inst_10 : NormedSpace ℝ F
inst_11 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (α := E × F) (_m := Prod.instMeasurableSpace) (toLp p) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
inst_1 : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
mF : MeasurableSpace F
inst_5 : NormedAddCommGroup F
inst_6 : CompleteSpace F
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_9 : NormedSpace ℝ E
inst_10 : NormedSpace ℝ F
inst_11 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (β := E × F) (fun (ω : Ω) ↦ (X ω, Y ω)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ IsProbabilityMeasure P

Tactic:
have := hX.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥∅) ↦ E) (Finset.restrict (π := fun (i : ι) ↦ Ω → E) ∅ X) P
empty :
  ∀ (x : StrongDual ℝ E),
    charFunDual (mE := inst) (Measure.map (∑ i ∈ ∅, X i) P) x =
      (∏ i ∈ ∅, charFunDual (mE := inst) (Measure.map (X i) P)) x
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ ∅, X i) P))
    (∏ i ∈ ∅, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
ext
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
mX : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥∅) ↦ E) (Finset.restrict (π := fun (i : ι) ↦ Ω → E) ∅ X) P
x : StrongDual ℝ E
⊢ charFunDual (mE := inst) (Measure.map (∑ i ∈ ∅, X i) P) x =
    (∏ i ∈ ∅, charFunDual (mE := inst) (Measure.map (X i) P)) x

Tactic:
simp [show (0 : Ω → E) = fun _ ↦ 0 from rfl]

Premises used: rfl
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ Insert.insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(Insert.insert i s)) ↦ E) ((Insert.insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
insert : ∀ i ∈ s, AEMeasurable (X i) P
insert₁ : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
insert₂ : AEMeasurable (X i) P
insert₃ : AEMeasurable.{u_1, u_3} (β := E) (∑ x ∈ s, X x) P
insert₄ : X i ⟂ᵢ[P] ∑ x ∈ s, X x
⊢ Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ Insert.insert i s, X i) P))
    (∏ i ∈ Insert.insert i s, charFunDual (mE := inst) (Measure.map (X i) P))

Tactic:
rw [Finset.sum_insert hi, IndepFun.charFunDual_map_add_eq_mul, Finset.prod_insert hi, hs]

Premises used: Finset.prod_insert, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, Finset.sum_insert
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ ∀ i ∈ s, AEMeasurable (X i) P

Tactic:
fun i hi ↦ (mX i (mem_insert_of_mem hi))

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ ∀ i ∈ s, AEMeasurable (X i) P

Tactic:
exact fun i hi ↦ (mX i (mem_insert_of_mem hi))

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
x : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄,
    Eq.{u_2 + 1} (α := ↥(insert i s))
        ((fun (x : ↥s) ↦ (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯ : ↥(insert i s))) x)
        ((fun (x : ↥s) ↦ (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯ : ↥(insert i s))) a₂) →
      x = a₂

Tactic:
simp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P

Tactic:
exact hX.precomp (g := fun x : s ↦ ⟨x.1, mem_insert_of_mem x.2⟩) (fun _ ↦ by simp)

Premises used: ProbabilityTheory.iIndepFun.precomp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ AEMeasurable (X i) P

Tactic:
mX i (mem_insert_self i s)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ AEMeasurable (X i) P

Tactic:
exact mX i (mem_insert_self i s)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ AEMeasurable.{u_1, u_3} (β := E) (∑ x ∈ s, X x) P

Tactic:
Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))

Premises used: Finset.mem_insert_of_mem, Finset.aemeasurable_sum
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ AEMeasurable.{u_1, u_3} (β := E) (∑ x ∈ s, X x) P

Tactic:
exact Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))

Premises used: Finset.mem_insert_of_mem, Finset.aemeasurable_sum
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ Insert.insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(Insert.insert i s)) ↦ E) ((Insert.insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
insert : (∑ x ∈ s, X x) ⟂ᵢ[P] X i
⊢ X i ⟂ᵢ[P] ∑ x ∈ s, X x

Tactic:
symm
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
⊢ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i ⋯ ∉ {x : ↥(insert i s) | (↑x : ι) ∈ s}

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
h : Eq (α := Ω → E) (∑ x ∈ s, X x) (∑ j : ↥(insert i s) with (↑j : ι) ∈ s, X (↑j : ι))
⊢ (∑ x ∈ s, X x) ⟂ᵢ[P] X i

Tactic:
convert!
      iIndepFun.indepFun_finsetSum_of_notMem₀ (i := ⟨i, mem_insert_self i s⟩) (f :=
        fun (x : (insert i s : Finset ι)) ↦ X x.1) (s := {x | x.1 ∈ s}) hX (fun i ↦ (mX i.1 i.2))
        (by simpa)

Premises used: ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem₀, Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s_1 : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  ∀ (mX : ∀ i ∈ s, AEMeasurable (X i) P)
    (hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P),
    Eq.{u_3 + 1} (α := (L : StrongDual ℝ E) → ℂ) (charFunDual (mE := inst) (Measure.map (∑ i ∈ s, X i) P))
      (∏ i ∈ s, charFunDual (mE := inst) (Measure.map (X i) P))
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun (β := fun (x : ↥(insert i s)) ↦ E) ((insert i s).restrict (π := fun (i : ι) ↦ Ω → E) X) P
e : ↥(insert i s) → ι := Subtype.val (p := fun (x : ι) ↦ x ∈ insert i s)
⊢ Eq (α := Ω → E) (∑ j ∈ s, X j) (∑ i_1 : ↥(insert i s) with (↑i_1 : ι) ∈ s, X (↑i_1 : ι))

Tactic:
(Finset.sum_of_injOn Subtype.val ?_ ?_ ?_ ?_).symm

Premises used: Finset.sum_of_injOn, Eq.symm, Subtype.val