awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
c : E
⊢ ∫ (x : ℝ) in a..b, c = (b - a) • c

Tactic:
simp only [integral_const', Real.volume_Ioc, ENNReal.toReal_ofReal', ← neg_sub b,
    max_zero_sub_eq_self, measureReal_def]

Premises used: neg_sub, Real.volume_Ioc, intervalIntegral.integral_const', MeasureTheory.measureReal_def, max_zero_sub_eq_self, ENNReal.toReal_ofReal'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
c : ℝ≥0∞
⊢ ∫ (x : ℝ) in a..b, f x ∂c • μ = HSMul.hSMul (β := E) c.toReal (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, Measure.restrict_smul, integral_smul_measure, smul_sub]

Premises used: MeasureTheory.Measure.restrict_smul, intervalIntegral, intervalIntegral.integral_smul_measure, smul_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_8
inst : RCLike 𝕜
a b : ℝ
μ : Measure ℝ
f : ℝ → ℝ
⊢ Eq.{u_8 + 1} (α := 𝕜) (∫ (x : ℝ) in a..b, (↑(f x) : 𝕜) ∂μ) (↑(∫ (x : ℝ) in a..b, f x ∂μ) : 𝕜)

Tactic:
simp only [intervalIntegral, integral_ofReal, RCLike.ofReal_sub]

Premises used: RCLike.ofReal_sub, intervalIntegral, integral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in a..b, (↑(f x) : ℂ) ∂μ = (↑(∫ (x : ℝ) in a..b, f x ∂μ) : ℂ)

Tactic:
RCLike.intervalIntegral_ofReal

Premises used: intervalIntegral, RCLike.intervalIntegral_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
simp_rw :
  (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, (φ x : (a : F) → E) v ∂μ)
simp_rw₁ :
  (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) ((∫ (x : ℝ) in Ι a b, φ x ∂μ : (a : F) → E) v : E)
simp_rw₂ :
  HSMul.hSMul (α := ℝ) (β := (a : F) → E) (if a ≤ b then 1 else -1) (⇑(∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) ((∫ (x : ℝ) in Ι a b, φ x ∂μ : (a : F) → E) v : E)
⊢ Eq.{u_5 + 1} (α := E) ((∫ (x : ℝ) in a..b, φ x ∂μ : (a : F) → E) v : E)
    (∫ (x : ℝ) in a..b, (φ x : (a : F) → E) v ∂μ : E)

Tactic:
simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, ContinuousLinearMap.integral_apply, ContinuousLinearMap.coe_smul', IntervalIntegrable.def', Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace F
inst_8 : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
simp_rw :
  HSub.hSub (α := F) (∫ (x : ℝ) in Ioc a b, (L : (a : E) → F) (f x) ∂μ)
      (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
simp_rw₁ :
  HSub.hSub (α := F) (β := F) ((L : (a : E) → F) (∫ (x : ℝ) in Ioc a b, f x ∂μ) : F)
      (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ : F) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
simp_rw₂ :
  HSub.hSub (α := F) (β := F) ((L : (a : E) → F) (∫ (x : ℝ) in Ioc a b, f x ∂μ) : F)
      ((L : (a : E) → F) (∫ (x : ℝ) in Ioc b a, f x ∂μ) : F) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
⊢ Eq.{u_6 + 1} (α := F) (∫ (x : ℝ) in a..b, (L : (a : E) → F) (f x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : ℝ) in a..b, f x ∂μ) : F)

Tactic:
simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]

Premises used: ContinuousLinearMap.map_sub, intervalIntegral, And.right, And.left, ContinuousLinearMap.integral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_8
inst : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (RCLike.re : (a : 𝕜) → ℝ) (f x) ∂μ : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) : ℝ)

Tactic:
RCLike.reCLM.intervalIntegral_comp_comm hf

Premises used: ContinuousLinearMap.intervalIntegral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_8
inst : RCLike 𝕜
f : ℝ → 𝕜
a b : ℝ
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (RCLike.im : (a : 𝕜) → ℝ) (f x) ∂μ : ℝ)
    ((RCLike.im : (a : 𝕜) → ℝ) (∫ (x : ℝ) in a..b, f x ∂μ) : ℝ)

Tactic:
RCLike.imCLM.intervalIntegral_comp_comm hf

Premises used: ContinuousLinearMap.intervalIntegral_comp_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c

Tactic:
have A : MeasurableEmbedding fun x => x * c :=
    (Homeomorph.mulRight₀ c hc).isClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
rw :
  HSMul.hSMul (β := E) c⁻¹
    (∫ (x : ℝ) in a * c..b * c,
      f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))
| HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a * c..b * c, f x)

Tactic:
rw [← Real.smul_map_volume_mul_right hc]

Premises used: Real.smul_map_volume_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
conv_rhs :
  ∫ (x : ℝ) in a..b, f (x * c) =
    HSMul.hSMul (β := E) c⁻¹
      (∫ (x : ℝ) in a * c..b * c,
        f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))
⊢ ∫ (x : ℝ) in a..b, f (x * c) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a * c..b * c, f x)

Tactic:
conv_rhs => rw [← Real.smul_map_volume_mul_right hc]

Premises used: Real.smul_map_volume_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
simp_rw :
  HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    HSMul.hSMul (β := E) c⁻¹
      (∫ (x : ℝ) in a * c..b * c,
        f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))

Tactic:
simp_rw [integral_smul_measure, intervalIntegral, A.setIntegral_map,
    ENNReal.toReal_ofReal (abs_nonneg c)]

Premises used: intervalIntegral, intervalIntegral.integral_smul_measure, ENNReal.toReal_ofReal, MeasurableEmbedding.setIntegral_map, abs_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
inl :
  ∀ (h : c < 0),
    HSub.hSub (α := E)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
      c⁻¹ •
        |c| •
          HSub.hSub (α := E)
            (@integral _ _ _ _ Real.measurableSpace
              (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
            (@integral _ _ _ _ Real.measurableSpace
              (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
inr :
  ∀ (h : 0 < c),
    HSub.hSub (α := E)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
      c⁻¹ •
        |c| •
          HSub.hSub (α := E)
            (@integral _ _ _ _ Real.measurableSpace
              (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
            (@integral _ _ _ _ Real.measurableSpace
              (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))

Tactic:
rcases hc.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
h : c < 0
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))

Tactic:
simp [h, mul_div_cancel_right₀, hc, abs_of_neg,
      Measure.restrict_congr_set (α := ℝ) (μ := volume) Ico_ae_eq_Ioc]

Premises used: MeasureTheory.Measure.restrict_congr_set, abs_of_neg, MeasureTheory.Ico_ae_eq_Ioc, mul_div_cancel_right₀
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
h : 0 < c
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))

Tactic:
simp [h, mul_div_cancel_right₀, hc, abs_of_pos]

Premises used: mul_div_cancel_right₀, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
simp [hc, integral_comp_mul_right]

Premises used: intervalIntegral.integral_comp_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
simp [hc, integral_comp_mul_right]

Premises used: intervalIntegral.integral_comp_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f x)

Tactic:
simpa only [mul_comm c] using integral_comp_mul_right f hc

Premises used: mul_comm, intervalIntegral.integral_comp_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
simp [hc, integral_comp_mul_left]

Premises used: intervalIntegral.integral_comp_mul_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
simp [hc, integral_comp_mul_left]

Premises used: intervalIntegral.integral_comp_mul_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (x / c) = HSMul.hSMul (β := E) c (∫ (x : ℝ) in a / c..b / c, f x)

Tactic:
simpa only [inv_inv] using integral_comp_mul_right f (inv_ne_zero hc)

Premises used: inv_inv, inv_ne_zero, intervalIntegral.integral_comp_mul_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
simp [hc, integral_comp_div]

Premises used: intervalIntegral.integral_comp_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
simp [hc, integral_comp_div]

Premises used: intervalIntegral.integral_comp_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + d
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (x + d))
    (∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun (x : ℝ) ↦ x + d) volume)

Tactic:
simp [intervalIntegral, A.setIntegral_map]

Premises used: intervalIntegral, MeasurableEmbedding.setIntegral_map
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + d
rw rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a + d..b + d, f x) (∫ (x : ℝ) in a + d..b + d, f x)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun (x : ℝ) ↦ x + d) volume)
    (∫ (x : ℝ) in a + d..b + d, f x)

Tactic:
rw [map_add_right_eq_self]

Premises used: MeasureTheory.map_add_right_eq_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (d + x)) (∫ (x : ℝ) in d + a..d + b, f x)

Tactic:
simpa only [add_comm d] using integral_comp_add_right f d

Premises used: add_comm, intervalIntegral.integral_comp_add_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
rw : ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (x + d))
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (c * x + d)) (∫ (x : ℝ) in a..b, f (c * x + d))
⊢ ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a + d..c * b + d, f x)

Tactic:
rw [← integral_comp_add_right, ← integral_comp_mul_left _ hc]

Premises used: intervalIntegral.integral_comp_mul_left, intervalIntegral.integral_comp_add_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
neg :
  ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
simp [hc, integral_comp_mul_add]

Premises used: intervalIntegral.integral_comp_mul_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
simp [hc, integral_comp_mul_add]

Premises used: intervalIntegral.integral_comp_mul_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
rw : ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (d + x))
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (d + c * x)) (∫ (x : ℝ) in a..b, f (d + c * x))
⊢ ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + c * a..d + c * b, f x)

Tactic:
rw [← integral_comp_add_left, ← integral_comp_mul_left _ hc]

Premises used: intervalIntegral.integral_comp_mul_left, intervalIntegral.integral_comp_add_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
neg :
  ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
simp [hc, integral_comp_add_mul]

Premises used: intervalIntegral.integral_comp_add_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
simp [hc, integral_comp_add_mul]

Premises used: intervalIntegral.integral_comp_add_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (x / c + d) = HSMul.hSMul (β := E) c (∫ (x : ℝ) in a / c + d..b / c + d, f x)

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_add f (inv_ne_zero hc) d

Premises used: inv_inv, inv_ne_zero, intervalIntegral.integral_comp_mul_add, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
pos :
  ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
neg :
  ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : c = 0
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
simp [hc, integral_comp_div_add]

Premises used: intervalIntegral.integral_comp_div_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
hc : ¬c = 0
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x

Tactic:
simp [hc, integral_comp_div_add]

Premises used: intervalIntegral.integral_comp_div_add