awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
x : ℝ
⊢ f (c * (x * c⁻¹)) = f x
have h₁ : c * (x * c⁻¹) = x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
⊢ (fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]
have h₁ : [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
Tactic: rw [preimage_mul_const_uIcc (inv_ne_zero hc)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
Tactic: have h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ⊤ := by
    rw [min_sub_sub_right, sub_add, sub_self, sub_zero]
    exact h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have inr : ∀
  (this :
    ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞)
      (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞) (hab : a ≤ b),
      IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c))
  (hab : ¬a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
Tactic: wlog hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞)
        (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞) (hab : a ≤ b),
        IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c))
    (hab : ¬a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have wlog : ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
  (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
Tactic: wlog hab : a ≤ b generalizing a b
Cleared hypotheses: hf, h, h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have apply : ‖f (min b a)‖ₑ ≠ ∞
Tactic: apply IntervalIntegrable.symm (this hf.symm ?_ ?_ (le_of_not_ge hab))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
apply : ‖f (min b a)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have apply₁ : ‖f (min (b - c) (a - c) + c)‖ₑ ≠ ∞
Tactic: apply IntervalIntegrable.symm (this hf.symm ?_ ?_ (le_of_not_ge hab))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
Tactic: rw [intervalIntegrable_iff' h] at hf
Cleared hypotheses: hf, h, h', hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
have rw : IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume
Tactic: rw [intervalIntegrable_iff' h'] at ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume
have A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
Tactic: have A : MeasurableEmbedding fun x => x + c :=
    (Homeomorph.addRight c).isClosedEmbedding.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume
have hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
Tactic: rw [← map_add_right_eq_self volume c] at hf
Cleared hypotheses: hf, h, h', hab, A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume
have h₁ : [[a - c, b - c]] = (fun (x : ℝ) ↦ x + c) ⁻¹' [[a, b]]
Tactic: convert! (MeasurableEmbedding.integrableOn_map_iff A).mp hf using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
⊢ [[a - c, b - c]] = (fun (x : ℝ) ↦ x + c) ⁻¹' [[a, b]]
have h₁ : [[a - c, b - c]] = [[a - c, b - c]]
Tactic: rw [preimage_add_const_uIcc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume a b
have this : ‖f (min (a + c) (b + c))‖ₑ ≠ ∞
Tactic: have : ‖f (min (a + c) (b + c))‖ₑ ≠ ⊤ := by rwa [min_add_add_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c + x)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b
have simp_rw : IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b
Tactic: simp_rw [add_comm c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b
have rw : IntervalIntegrable f volume (a - c + c) (b - c + c) ↔ IntervalIntegrable f volume a b
Tactic: rw [IntervalIntegrable.comp_add_right_iff (by grind)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x - c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b
have simp_rw : IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + -c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + -c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b
have rw : IntervalIntegrable f volume (a + c + -c) (b + c + -c) ↔ IntervalIntegrable f volume a b
Tactic: rw [IntervalIntegrable.comp_add_right_iff (by grind)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume a b ↔ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-a) (-b)
have rw : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
  IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-a) (-b)
Tactic: rw [← comp_mul_left_iff (neg_ne_zero.2 one_ne_zero) h (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntervalIntegrable u μ a b
have rw : IntegrableOn u (Ι a b) μ
Tactic: rw [intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume 0 t
have inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t
have inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t
have inr₁ : ∀ (h : 0 < t), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable f volume 0 t
have inl : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
Tactic: rw [IntervalIntegrable.iff_comp_neg ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have arg : fun (x : ℝ) ↦ f (-x)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t_1 : ℝ
ht : ‖f (min 0 t_1)‖ₑ ≠ ∞
h : t_1 < 0
t : ℝ
| f (-t)
have h₁ : f t
Tactic: rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have h₁ : ∀ (t : ℝ), f t
Tactic: arg 1; intro t; rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have inl : IntervalIntegrable f volume (-0) (-t)
Tactic: conv => arg 1; intro t; rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t = 0
⊢ IntervalIntegrable f volume 0 t
have inr : IntervalIntegrable f volume 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume 0 t
have inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t
have inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t
have inr₁ : ∀ (h : 0 < t), IntervalIntegrable f volume 0 t
Tactic: rcases lt_trichotomy t 0 with h | h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable f volume 0 t
have inl : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
Tactic: rw [IntervalIntegrable.iff_comp_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have arg : fun (x : ℝ) ↦ f (-x)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t_1 : ℝ
ht : ‖f (min 0 t_1)‖ₑ ≠ ∞
h : t_1 < 0
t : ℝ
| f (-t)
have h₁ : -f t
Tactic: rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have h₁ : ∀ (t : ℝ), -f t
Tactic: arg 1; intro t; rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
have inl : IntervalIntegrable.{u_5} (ε := E) (fun (t : ℝ) ↦ -f t) volume (-0) (-t)
Tactic: conv => arg 1; intro t; rw [← h₁f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (t : ℝ) ↦ -f t) volume (-0) (-t)
have inl : IntervalIntegrable f volume (-0) (-t)
Tactic: apply IntervalIntegrable.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t = 0
⊢ IntervalIntegrable f volume 0 t
have inr : IntervalIntegrable f volume 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have pos : ∀ (h : a ≤ b), ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
pos : ∀ (h : a ≤ b), ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ)
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have neg : ∀ (h : ¬a ≤ b), ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (-1) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have simp_rw : norm (E := ℝ) (if a ≤ b then 1 else -1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
  norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic: simp_rw [intervalIntegral_eq_integral_uIoc, norm_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ norm (E := ℝ) (if a ≤ b then 1 else -1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have pos : a ≤ b →
  norm (E := ℝ) 1 * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
pos :
  a ≤ b →
    norm (E := ℝ) 1 * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
      norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
⊢ norm (E := ℝ) (if a ≤ b then 1 else -1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have neg : ¬a ≤ b →
  norm (E := ℝ) (-1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ} (∫ (x : ℝ) in a..b, f x ∂μ)
have rw : Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
  (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ))
Tactic: rw [intervalIntegral_eq_integral_uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ))
have pos : a ≤ b →
  Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ))
Tactic: split_ifs