awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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 μ
have rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * g x) μ a b
Tactic: rw [← intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
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
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hfg : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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 μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have 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 ∂μ
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
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 ∂μ
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have h' : ∫ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (goal)
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
have rw : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → 0 ≤ g x
Tactic: rw [ae_restrict_iff' measurableSet_uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue (hypothesis)
Goal:
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ x ∈ Ι a b, 0 ≤ g x
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
have hg0_ae : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ
have refine : ∀ (x : ℝ), ∃! g : ↥(zmultiples T), g +ᵥ x ∈ Ioc t (t + T)
Tactic: refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
⊢ ∃! g : ↥(zmultiples T), g +ᵥ x ∈ Ioc t (t + T)
have this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) sorry)
Tactic: have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
    (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have refine : ∃! x_1 : ℤ, codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) sorry x_1 +ᵥ x ∈ Ioc t (t + T)
Tactic: refine this.existsUnique_iff.2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
⊢ IsAddFundamentalDomain (↥(AddSubgroup.op (zmultiples T))) (Ioc t (t + T)) μ
have refine : ∀ (x : ℝ), ∃! g : ↥(AddSubgroup.op (zmultiples T)), g +ᵥ x ∈ Ioc t (t + T)
Tactic: refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
⊢ ∃! g : ↥(AddSubgroup.op (zmultiples T)), g +ᵥ x ∈ Ioc t (t + T)
have this : Bijective (codRestrict (fun (n : ℤ) ↦ n • T) (↑(zmultiples T) : Set ℝ) sorry)
Tactic: have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
    (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
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)
have 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 ℝ) sorry)
        x_1)
      x ∈
    Ioc t (t + T)
Tactic: refine (AddSubgroup.equivOp _).bijective.comp this |>.existsUnique_iff.2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
⊢ AddQuotientMeasureEqMeasurePreimage (G := ↥(AddSubgroup.op (zmultiples T))) (α := ℝ) volume volume
have h : addCovolume ↥(AddSubgroup.op (zmultiples T)) ℝ volume =
  ((volume : Measure (AddCircle T)) : (a : Set (ℝ ⧸ zmultiples T)) → ℝ≥0∞) univ
Tactic: apply MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
have hT' : |T| = T
Tactic: have hT' : |T| = T := abs_eq_self.mpr hT.out.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
have rw : Icc (-ε) ε ⊆ I
Tactic: rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ y ∈ I
have left : -(T / 2) < y
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
left : -(T / 2) < y
⊢ y ∈ I
have right : y ≤ T / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ -(T / 2) < y
have linarith : y ≤ -(T / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : y ≤ -(T / 2) → 2 / 2 = 1
⊢ -(T / 2) < y
have linarith₁ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : y ≤ -(T / 2) → 2 / 2 = 1
linarith₁ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(T / 2) < y
have linarith₂ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : y ≤ -(T / 2) → 2 / 2 = 1
linarith₁ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : y ≤ -(T / 2) → 2 / 2 = 1
linarith₄ : y ≤ -(T / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : y ≤ -(T / 2) → GT.gt (α := ℝ) 2 0
⊢ -(T / 2) < y
have linarith₆ : y ≤ -(T / 2) → 2 * ε - 1 * T + 2 * (-ε - y) + (2 * y - -(1 * T)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ y ≤ T / 2
have linarith : T / 2 < y → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : T / 2 < y → 2 / 2 = 1
⊢ y ≤ T / 2
have linarith₁ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : T / 2 < y → 2 / 2 = 1
linarith₁ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
⊢ y ≤ T / 2
have linarith₂ : T / 2 < y → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
linarith : T / 2 < y → 2 / 2 = 1
linarith₁ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : T / 2 < y → GT.gt (α := ℝ) 2 0
linarith₃ : T / 2 < y → 2 / 2 = 1
linarith₄ : T / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : T / 2 < y → GT.gt (α := ℝ) 2 0
⊢ y ≤ T / 2
have linarith₆ : T / 2 < y → 2 * ε - 1 * T + 2 * (y - ε) + (1 * T - 2 * y) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
have h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
Tactic: have h₁ : ε < T / 2 → Metric.closedBall (0 : ℝ) ε ∩ I = Metric.closedBall (0 : ℝ) ε := by
    intro hε
    rw [inter_eq_left, Real.closedBall_eq_Icc, zero_sub, zero_add]
    rintro y ⟨hy₁, hy₂⟩; constructor <;> linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
| if ε < T / 2 then Metric.closedBall 0 ε else I
have rw : if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
Tactic: rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
have conv_rhs : preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
  if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
Tactic: conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < |T| / 2 then Metric.closedBall 0 ε ∩ I else I
have hs : I ⊆ Metric.closedBall 0 (|T| / 2)
Tactic: apply coe_real_preimage_closedBall_inter_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
have h₂ : preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
  if ε < T / 2 then Metric.closedBall 0 ε else I
Tactic: have h₂ : (↑) ⁻¹' Metric.closedBall (0 : AddCircle T) ε ∩ I =
      if ε < T / 2 then Metric.closedBall (0 : ℝ) ε else I := by
    conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
    apply coe_real_preimage_closedBall_inter_eq
    simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ -(T / 2) + T = T / 2
have linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
⊢ -(T / 2) + T = T / 2
have linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(T / 2) + T = T / 2
have linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
⊢ -(T / 2) + T = T / 2
have linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
⊢ -(T / 2) + T = T / 2
have linarith₆ : T / 2 < -(T / 2) + T → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
linarith₆ : T / 2 < -(T / 2) + T → 2 / 2 = 1
⊢ -(T / 2) + T = T / 2
have linarith₇ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
linarith₆ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₇ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₉ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(T / 2) + T = T / 2
have linarith₁₀ : T / 2 < -(T / 2) + T → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
linarith : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₁ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(T / 2) + T < T / 2 → 2 / 2 = 1
linarith₃ : -(T / 2) + T < T / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : -(T / 2) + T < T / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : -(T / 2) + T < T / 2 → -(1 * T) + 2 * T - 1 * T = 0
linarith₆ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₇ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : T / 2 < -(T / 2) + T → 2 / 2 = 1
linarith₉ : T / 2 < -(T / 2) + T → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : T / 2 < -(T / 2) + T → GT.gt (α := ℝ) 2 0
⊢ -(T / 2) + T = T / 2
have linarith₁₁ : T / 2 < -(T / 2) + T → 1 * T - (-(1 * T) + 2 * T) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
have rw : (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
Tactic: rw [addHaar_closedBall_center, add_projection_respects_measure T (-(T / 2))
    measurableSet_closedBall, (by linarith : -(T / 2) + T = T / 2), h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
have pos : ∀ (hε : ε < T / 2),
  (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
Tactic: by_cases hε : ε < T / 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
pos :
  ∀ (hε : ε < T / 2),
    (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
have neg : ∀ (hε : ¬ε < T / 2),
  (volume : (a : Set ℝ) → ℝ≥0∞) (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
Tactic: by_cases hε : ε < T / 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
⊢ 2 * ε ≤ T
have linarith : T < 2 * ε → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ :
  preimage (β := AddCircle T) QuotientAddGroup.mk (Metric.closedBall 0 ε) ∩ I =
    if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ε < T / 2
linarith : T < 2 * ε → 2 / 2 = 1
⊢ 2 * ε ≤ T
have linarith₁ : T < 2 * ε → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith