awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
neg :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
        (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
        ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ)
    (hab : ¬a < b), ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
wlog :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
wlog hab : a < b generalizing a b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : ¬a < b
⊢ b ≤ a

Tactic:
simp only [not_lt] at hab

Premises used: not_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f [[a, b]]
⊢ ContinuousOn f [[b, a]]

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
rwa rwa₁ rwa₂ rwa₃ : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι b a), 0 ≤ g x

Tactic:
rwa [uIoc_comm]

Premises used: Set.uIoc_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
⊢ ¬b = a

Tactic:
lia
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
neg :
  ∀ (c : ℝ) (c_in_uIcc : c ∈ [[b, a]]) (that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
obtain ⟨c, c_in_uIcc, that⟩ :=
      this (by rwa [uIcc_comm]) hg.symm (by rwa [uIoc_comm]) (by lia) (lt_of_le_of_ne' hab h)

Premises used: IntervalIntegrable.symm, lt_of_le_of_ne'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
c : ℝ
c_in_uIcc : c ∈ [[b, a]]
that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ
rwa rwa₁ rwa₂ rwa₃ : c ∈ [[b, a]]
⊢ c ∈ [[a, b]]

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
c : ℝ
c_in_uIcc : c ∈ [[b, a]]
that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ
⊢ ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simpa [integral_symm b a]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ} (hf : ContinuousOn f [[a, b]]) (hg : IntervalIntegrable g μ a b)
    (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) (h : ¬a = b) (hab : a < b),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : b ≤ a
c : ℝ
c_in_uIcc : c ∈ [[b, a]]
that : ∫ (x : ℝ) in b..a, f x * g x ∂μ = f c * ∫ (x : ℝ) in b..a, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
exact ⟨c, by rwa [uIcc_comm], by simpa [integral_symm b a]⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
⊢ s = Ioc a b

Tactic:
have hs : s = Ioc a b := uIoc_of_le hab.le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
⊢ s ⊆ [[a, b]]

Tactic:
have hs' : s ⊆ [[a, b]] := uIoc_subset_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
⊢ IsConnected s

Tactic:
simpa [hs] using isConnected_Ioc hab

Premises used: isConnected_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
⊢ IsConnected s

Tactic:
have hs_conn : IsConnected s := by simpa [hs] using isConnected_Ioc hab
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) μ a b
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ

Tactic:
rw [← intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) μ a b

Tactic:
hg.continuousOn_smul hf

Premises used: IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) μ a b

Tactic:
exact hg.continuousOn_smul hf

Premises used: IntervalIntegrable.continuousOn_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ

Tactic:
have hfg : IntegrableOn (fun x ↦ f x * g x) s μ := by
    rw [← intervalIntegrable_iff]
    exact hg.continuousOn_smul hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
rwa rwa₁ rwa₂ rwa₃ : IntervalIntegrable g μ a b
⊢ IntegrableOn g s μ

Tactic:
rwa [← intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
obtain :
  ∀ (c : ℝ) (hc : c ∈ s) (h : ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ),
    ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
obtain ⟨c, hc, h⟩ := exists_eq_const_mul_setIntegral_of_ae_nonneg
    hs_conn measurableSet_uIoc (hf.mono hs') (by rwa [← intervalIntegrable_iff]) hfg hg0

Premises used: measurableSet_uIoc, ContinuousOn.mono, exists_eq_const_mul_setIntegral_of_ae_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h_1 : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
c : ℝ
hc : c ∈ s
h : ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simpa [intervalIntegral.integral_of_le hab.le, hs] using h

Premises used: LT.lt.le, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h_1 : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
c : ℝ
hc : c ∈ s
h : ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
have h' : ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ := by
    simpa [intervalIntegral.integral_of_le hab.le, hs] using h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h_1 : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
c : ℝ
hc : c ∈ s
h : ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
h' : ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
⟨c, mem_of_subset_of_mem hs' hc, h'⟩

Premises used: Set.mem_of_subset_of_mem, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a_1 b_1 : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h_1 : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
hfg : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) s μ
c : ℝ
hc : c ∈ s
h : ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
h' : ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
exact ⟨c, mem_of_subset_of_mem hs' hc, h'⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
rw : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x

Tactic:
rw [ae_restrict_iff' measurableSet_uIoc]

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → 0 ≤ g x

Tactic:
ae_of_all μ hg0

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → 0 ≤ g x

Tactic:
exact ae_of_all μ hg0

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x

Tactic:
have hg0_ae : ∀ᵐ x ∂(μ.restrict (Ι a b)), 0 ≤ g x := by
    rw [ae_restrict_iff' measurableSet_uIoc]
    exact ae_of_all μ hg0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
hg0_ae : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
exists_eq_const_mul_intervalIntegral_of_ae_nonneg hf hg hg0_ae

Premises used: exists_eq_const_mul_intervalIntegral_of_ae_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
hg0_ae : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
exact exists_eq_const_mul_intervalIntegral_of_ae_nonneg hf hg hg0_ae

Premises used: exists_eq_const_mul_intervalIntegral_of_ae_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
a : ℝ
⊢ Measurable (α := ℝ) (β := AddCircle a) QuotientAddGroup.mk

Tactic:
Continuous.measurable <| AddCircle.continuous_mk' a

Premises used: AddCircle.continuous_mk', Continuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ

Tactic:
IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Premises used: nullMeasurableSet_Ioc, Set.Mem, MeasureTheory.IsAddFundamentalDomain.mk'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
refine : ∀ (x : ℝ), ∃! g : ↥(zmultiples T), g +ᵥ x ∈ Ioc t (t + T)
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Premises used: nullMeasurableSet_Ioc, MeasureTheory.IsAddFundamentalDomain.mk'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
⊢ Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)

Tactic:
have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
    (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
⊢ ∃! g : ↥(zmultiples T), g +ᵥ x ∈ Ioc t (t + T)

Tactic:
this.existsUnique_iff.2 ?_

Premises used: Iff.mpr, Function.Bijective.existsUnique_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
refine : ∃! x_1 : ℤ, codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)
⊢ ∃! g : ↥(zmultiples T), g +ᵥ x ∈ Ioc t (t + T)

Tactic:
refine this.existsUnique_iff.2 ?_

Premises used: Iff.mpr, Function.Bijective.existsUnique_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
⊢ ∃! x_1 : ℤ, codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)

Tactic:
simpa only [add_comm x] using existsUnique_add_zsmul_mem_Ioc hT x t

Premises used: existsUnique_add_zsmul_mem_Ioc, add_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(AddSubgroup.op (zmultiples T))) (Ioc t (t + T)) μ

Tactic:
IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Premises used: nullMeasurableSet_Ioc, Set.Mem, MeasureTheory.IsAddFundamentalDomain.mk', AddSubgroup.op
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
refine : ∀ (x : ℝ), ∃! g : ↥(AddSubgroup.op (zmultiples T)), g +ᵥ x ∈ Ioc t (t + T)
⊢ IsAddFundamentalDomain (↥(AddSubgroup.op (zmultiples T))) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Premises used: nullMeasurableSet_Ioc, MeasureTheory.IsAddFundamentalDomain.mk'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
⊢ ∃! g : ↥(AddSubgroup.op (zmultiples T)), g +ᵥ x ∈ Ioc t (t + T)

Tactic:
(AddSubgroup.equivOp _).bijective.comp this |>.existsUnique_iff.2 ?_

Premises used: Iff.mpr, Equiv.bijective, AddSubgroup.equivOp, Function.Bijective.comp, Function.Bijective.existsUnique_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
refine :
  ∃! x_1 : ℤ,
    HVAdd.hVAdd (α := ↥(AddSubgroup.op (zmultiples T)))
        (((⇑(equivOp (zmultiples T)) : (a : ↥(zmultiples T)) → ↥(zmultiples T).op) ∘
            codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
          x_1)
        x ∈
      Ioc t (t + T)
⊢ ∃! g : ↥(AddSubgroup.op (zmultiples T)), g +ᵥ x ∈ Ioc t (t + T)

Tactic:
refine (AddSubgroup.equivOp _).bijective.comp this |>.existsUnique_iff.2 ?_

Premises used: Iff.mpr, Equiv.bijective, AddSubgroup.equivOp, Function.Bijective.comp, Function.Bijective.existsUnique_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
⊢ ∃! x_1 : ℤ,
    HVAdd.hVAdd (α := ↥(AddSubgroup.op (zmultiples T)))
        (((⇑(equivOp (zmultiples T)) : (a : ↥(zmultiples T)) → ↥(zmultiples T).op) ∘
            codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) ⋯)
          x_1)
        x ∈
      Ioc t (t + T)

Tactic:
simpa using existsUnique_add_zsmul_mem_Ioc hT x t

Premises used: existsUnique_add_zsmul_mem_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T)
      ((addHaarMeasure ⊤ : (a : Set (AddCircle T)) → ℝ≥0∞) (↑⊤ : Set (AddCircle T)) : ℝ≥0∞) =
    ENNReal.ofReal T

Tactic:
simp [addHaarMeasure_self (G := AddCircle T), -PositiveCompacts.coe_top]

Premises used: TopologicalSpace.PositiveCompacts.coe_top, MeasureTheory.Measure.addHaarMeasure_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ ENNReal.ofReal T ≠ 0

Tactic:
simp [hT.out]

Premises used: Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ LT.lt (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
h :
  addCovolume ↥(AddSubgroup.op (zmultiples T)) ℝ volume =
    ((volume : Measure (AddCircle T)) : (a : Set (ℝ ⧸ zmultiples T)) → ℝ≥0∞) univ
⊢ AddQuotientMeasureEqMeasurePreimage (G := ↥(AddSubgroup.op (zmultiples T))) (α := ℝ) volume volume

Tactic:
apply MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage

Premises used: MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ addCovolume ↥(AddSubgroup.op (zmultiples T)) ℝ volume =
    ((volume : Measure (AddCircle T)) : (a : Set (ℝ ⧸ zmultiples T)) → ℝ≥0∞) univ

Tactic:
simp [(isAddFundamentalDomain_Ioc' hT.out 0).covolume_eq_volume, AddCircle.measure_univ]

Premises used: AddCircle.measure_univ, MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume, OfNat.ofNat, isAddFundamentalDomain_Ioc', Fact.out
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
Goal:
T : ℝ
hT : Fact (0 < T)
t : ℝ
⊢ MeasurePreserving (β := AddCircle T) QuotientAddGroup.mk (Measure.restrict volume (Ioc t (t + T)))
    (volume : Measure (AddCircle T))

Tactic:
measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage
    volume (𝓕 := Ioc t (t + T)) (isAddFundamentalDomain_Ioc' hT.out _) _

Premises used: MeasureTheory.MeasureSpace.volume, measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage