awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_

Premises used: MeasureTheory.tendsto_setToFun_of_dominated_convergence, dite, MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ
refine_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a
refine_3 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
refine tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_

Premises used: MeasureTheory.tendsto_setToFun_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ

Tactic:
fun n => (h _ (self_le_add_left _ _)).1

Premises used: Set.Mem, setOf, self_le_add_left, And.left, HAdd.hAdd, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ

Tactic:
exact fun n => (h _ (self_le_add_left _ _)).1

Premises used: self_le_add_left, And.left, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a

Tactic:
fun n => (h _ (self_le_add_left _ _)).2

Premises used: Set.Mem, Filter.Eventually, setOf, self_le_add_left, And.right, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a

Tactic:
exact fun n => (h _ (self_le_add_left _ _)).2

Premises used: self_le_add_left, And.right, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
h₁ : ∀ (a : α), Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
filter_upwards [h_lim]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (a : α), Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
h₁ : ∀ (a : α) (h_lin : Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))), Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l
⊢ ∀ (a : α), Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
refine fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
a : α
h_lin : Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
h₁ h₂ h₃ h₄ : Tendsto x atTop l
⊢ Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l

Tactic:
rwa [tendsto_add_atTop_iff_nat]

Premises used: Filter.tendsto_add_atTop_iff_nat
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
x₀ : X
bound : α → ℝ
s : Set X
hfs_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (fs x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x₀
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x₀

Tactic:
tendsto_setToFun_filter_of_dominated_convergence hT bound ‹_› ‹_› ‹_› ‹_›

Premises used: ContinuousWithinAt, MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
x₀ : X
bound : α → ℝ
hfs_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (fs x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) x₀
⊢ ContinuousAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) x₀

Tactic:
tendsto_setToFun_filter_of_dominated_convergence hT bound ‹_› ‹_› ‹_› ‹_›

Premises used: ContinuousAt, MeasureTheory.tendsto_setToFun_filter_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x

Tactic:
continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_

Premises used: MeasureTheory.continuousWithinAt_setToFun_of_dominated
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
refine_1 : ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
refine_2 : ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
refine_3 : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x

Tactic:
refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_

Premises used: MeasureTheory.continuousWithinAt_setToFun_of_dominated
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ AEStronglyMeasurable (fs x) μ

Tactic:
hfs_meas x hx
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X | x ∈ s → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ AEStronglyMeasurable (fs x) μ) x} x} a
h₁ h₂ : ∀ (x : X) (hx : x ∈ s), AEStronglyMeasurable (fs x) μ
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx using hfs_meas x hx

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x_1 : X
hx_1 : x_1 ∈ s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

Tactic:
h_bound x hx
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X | x ∈ s → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) x} x} a
h₁ h₂ : ∀ (x : X) (hx : x ∈ s), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
a : α
ha : ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
⊢ ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x

Tactic:
ha x hx
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s) x} x_1 →
          Membership.mem (γ := Set α)
            {x_2 : α | (fun (a : α) ↦ ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x) x_2} x_1}
      a
h₁ h₂ :
  ∀ (a : α) (ha : ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s),
    ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x

Tactic:
filter_upwards [h_cont] with a ha using ha x hx
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
hfs_meas : ∀ (x : X), AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst_4, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ fs x a
⊢ Continuous[inst_4, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ setToFun μ T hT (fs x)

Tactic:
continuous_iff_continuousAt.mpr fun _ =>
    continuousAt_setToFun_of_dominated hT (Eventually.of_forall hfs_meas)
        (Eventually.of_forall h_bound) ‹_› <|
      h_cont.mono fun _ => Continuous.continuousAt

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.Eventually.mono, Continuous.continuousAt, MeasureTheory.continuousAt_setToFun_of_dominated, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
h : ∀ (i : Fin n), (torusMap c R θ - c) i = torusMap 0 R θ i
⊢ torusMap c R θ - c = torusMap 0 R θ

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
i : Fin n
⊢ (torusMap c R θ - c) i = torusMap 0 R θ i

Tactic:
simp [torusMap]

Premises used: torusMap
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ = c ↔ R = 0

Tactic:
simp [funext_iff, torusMap, exp_ne_zero]

Premises used: Complex.exp_ne_zero, torusMap, funext_iff