awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
refine : ⋃ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i)) : Filter ℝ≥0∞)

Tactic:
refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
      (partialSups_monotone f) (hC.partialSups_mem hf) ?_

Premises used: partialSups_monotone, MeasureTheory.IsSetRing.partialSups_mem, MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
rwa : ⨆ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C
rwa₁ rwa₂ rwa₃ rwa₄ : ⨆ (i : ℕ), f i ∈ C
⊢ ⋃ (i : ℕ), (partialSups f : (a : ℕ) → Set α) i ∈ C

Tactic:
rwa [← iSup_eq_iUnion, iSup_partialSups_eq]

Premises used: iSup_partialSups_eq, Set.iSup_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)

Tactic:
have h_tendsto : Tendsto (fun n ↦ m (partialSups f n)) atTop (𝓝 (m (⋃ i, f i))) := by
    rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]
    refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
      (partialSups_monotone f) (hC.partialSups_mem hf) ?_
    rwa [← iSup_eq_iUnion, iSup_partialSups_eq]
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
rw :
  Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))

Tactic:
rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]

Premises used: Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))

Tactic:
ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (k : ℕ) ↦ ∑ i ∈ Finset.range k, (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))

Tactic:
exact ENNReal.tendsto_nat_tsum _

Premises used: ENNReal.tendsto_nat_tsum
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))

Tactic:
have h_tendsto' : Tendsto (fun n ↦ ∑ i ∈ range (n + 1), m (f i)) atTop (𝓝 (∑' i, m (f i))) := by
    rw [tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (f i))) 1]
    exact ENNReal.tendsto_nat_tsum _
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
refine :
  ∀ (x : ℕ),
    LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) x) : ℝ≥0∞)
      (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
x : ℕ
rw :
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range (x + 1), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) x) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [partialSups_eq_biUnion_range]

Premises used: partialSups_eq_biUnion_range
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
x : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range (x + 1), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
addContent_biUnion_le hC (fun _ _ ↦ hf _)

Premises used: MeasureTheory.addContent_biUnion_le
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
x : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range (x + 1), f i) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
exact addContent_biUnion_le hC (fun _ _ ↦ hf _)

Premises used: MeasureTheory.addContent_biUnion_le
-- Module: Mathlib.MeasureTheory.Measure.AddContent
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
s : ℕ → Set α
hd : Pairwise (Disjoint on s)
hs : ∀ (i : ℕ), s i ∈ C
hm_iSup :
  ∀ ⦃s : ℕ → Set α⦄,
    (∀ (n : ℕ), s n ∈ C) →
      Monotone s →
        Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞)
          (⨆ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), accumulate s i) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t x : E
⊢ (innerProbChar t : (a : E) → ℂ) x = cexp ((↑⟪x, t⟫ : ℂ) * I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ Eq.{u_1 + 1} (α := E →ᵇ ℂ) (innerProbChar 0) 1

Tactic:
simp [innerProbChar]

Premises used: BoundedContinuousFunction.innerProbChar
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
L : StrongDual ℝ F
x : F
⊢ (probCharDual L : (a : F) → ℂ) x = cexp ((↑((L : (a : F) → ℝ) x) : ℂ) * I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
F : Type u_2
inst : SeminormedAddCommGroup F
inst_1 : NormedSpace ℝ F
⊢ Eq.{u_2 + 1} (α := F →ᵇ ℂ) (probCharDual 0) 1

Tactic:
simp [probCharDual]

Premises used: BoundedContinuousFunction.probCharDual
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
apply : ∀ g ∈ charPoly he hL, Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
⊢ P = P'

Tactic:
apply ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
      (separatesPoints_charPoly he he' hL hL')

Premises used: MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable, BoundedContinuousFunction.separatesPoints_charPoly
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
hg : g ∈ charPoly he hL
⊢ ∃ (w : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)

Tactic:
simp only [mem_charPoly] at hg

Premises used: BoundedContinuousFunction.mem_charPoly
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
hg :
  ∃ (w : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
obtain :
  ∀ (w : AddMonoidAlgebra ℂ W)
    (hw :
      Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)),
    Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
⊢ Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')

Tactic:
obtain ⟨w, hw⟩ := hg
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
rw :
  Eq (α := ℂ)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P')
⊢ Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')

Tactic:
rw [hw]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ ∀ (P : Measure V) [IsFiniteMeasure P],
    Eq (α := ℂ)
      (∫ (v : V),
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
      (∑ a ∈ w.support,
        ∫ (v : V),
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)

Tactic:
have hsum (P : Measure V) [IsFiniteMeasure P] :
      ∫ v, ∑ a ∈ w.support, w a * e (L v a) ∂P = ∑ a ∈ w.support, ∫ v, w a * e (L v a) ∂P :=
    integral_finsetSum w.support
      fun a ha => Integrable.const_mul (integrable P (char he hL a)) _