awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
have rw₁ : HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
  HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
Tactic: rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
    sub_neg_eq_add, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
have rw₂ : HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
  HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (-∫ (x : ℝ) in a..c, f x ∂μ)
Tactic: rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
    sub_neg_eq_add, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₂ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (-∫ (x : ℝ) in a..c, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
have rw₃ : HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
  HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ)
Tactic: rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
    sub_neg_eq_add, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₂ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (-∫ (x : ℝ) in a..c, f x ∂μ)
rw₃ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
have rw₄ : HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ) =
  HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ)
Tactic: rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
    sub_neg_eq_add, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : ∀
  (this :
    ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
      HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
  (hab : ¬a ≤ b),
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : ¬a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have wlog : ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog hab : a ≤ b generalizing a b
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
Tactic: rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₁ : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) =
  -HSub.hSub (α := E) (∫ (x : ℝ) in Iic a, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)
Tactic: rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Iic a, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₂ : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) =
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ)
Tactic: rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have ht : MeasurableSet (Ioc a b)
Tactic: rw [sub_eq_iff_eq_add', integral_of_le hab, ← setIntegral_union (Iic_disjoint_Ioc le_rfl),
    Iic_union_Ioc_eq_Iic hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
ht : MeasurableSet (Ioc a b)
hfs : IntegrableOn f (Iic a) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have hft : IntegrableOn f (Ioc a b) μ
Tactic: rw [sub_eq_iff_eq_add', integral_of_le hab, ← setIntegral_union (Iic_disjoint_Ioc le_rfl),
    Iic_union_Ioc_eq_Iic hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have inr : ∀
  (this :
    ∀ {a b : ℝ} (ha : IntegrableOn f (Ioi a) μ) (hb : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
      HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ)
  (hab : ¬a ≤ b),
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
Tactic: wlog hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (ha : IntegrableOn f (Ioi a) μ) (hb : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
        HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ)
    (hab : ¬a ≤ b),
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have wlog : ∀ {a b : ℝ} (ha : IntegrableOn f (Ioi a) μ) (hb : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
Tactic: wlog hab : a ≤ b generalizing a b
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Ioi a) μ) (hb : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
hab : ¬a ≤ b
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have inr : -∫ (x : ℝ) in b..a, f x ∂μ + HAdd.hAdd (α := E) (∫ (x : ℝ) in b..a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ) =
  ∫ (x : ℝ) in Ioi a, f x ∂μ
Tactic: rw [integral_symm, ← this hb ha (le_of_not_ge hab)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
Tactic: rw [integral_of_le hab, ← setIntegral_union Ioc_disjoint_Ioi_same measurableSet_Ioi
    (ha.mono_set Ioc_subset_Ioi_self) hb, Ioc_union_Ioi_eq_Ioi hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
Tactic: rw [integral_of_le hab, ← setIntegral_union Ioc_disjoint_Ioi_same measurableSet_Ioi
    (ha.mono_set Ioc_subset_Ioi_self) hb, Ioc_union_Ioi_eq_Ioi hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
Tactic: rw [integral_of_le hab, ← setIntegral_union Ioc_disjoint_Ioi_same measurableSet_Ioi
    (ha.mono_set Ioc_subset_Ioi_self) hb, Ioc_union_Ioi_eq_Ioi hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
have rw : IntegrableOn f (Ioi a) μ
Tactic: rw [integral_interval_add_Ioi _ hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
⊢ IntegrableOn f (Ioi a) μ
have pos : ∀ (h : a ≤ b), IntegrableOn f (Ioi a) μ
Tactic: by_cases! h : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
pos : ∀ (h : a ≤ b), IntegrableOn f (Ioi a) μ
⊢ IntegrableOn f (Ioi a) μ
have neg : ∀ (h : b < a), IntegrableOn f (Ioi a) μ
Tactic: by_cases! h : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : ∀
  (this :
    ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
      HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
  (hab : b < a),
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : b < a),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have wlog! : ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing a b
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₁ : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) =
  -HSub.hSub (α := E) (∫ (x : ℝ) in Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₂ : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) =
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have ha : IntegrableOn f (Iio a) μ
Tactic: have ha : IntegrableOn f (Iio a) μ := hf.mono_set (Iio_subset_Iio hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have h : IntegrableOn f (Ico a b) μ
Tactic: have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Iio_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw : ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a ∪ Ico a b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a ∪ Ico a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]