mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁹ : TopologicalSpace E
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
s : Set E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s

Tactic:
by
  set ι := Σ (l : StrongDual 𝕜 E), { c : ℝ // ∀ y ∈ s, re (l y) ≤ c }
  set l : ι → StrongDual 𝕜 E := fun lc ↦ lc.1
  set c : ι → ℝ := fun lc ↦ lc.2.val
  set hc : ∀ i, ∀ y ∈ s, re (l i y) ≤ c i := fun lc ↦ lc.2.prop
  have : Nonempty ι := ⟨0, 0, fun _ _ ↦ by simp⟩
  have : ⋂ i : ι, { x | re (l i x) ≤ c i } = s := by
    simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ hs₂
  obtain ⟨k, hk⟩ := eq_closed_inter_nat (fun i : ι ↦ { x | re (l i x) ≤ c i })
    (fun i ↦ isClosed_le (continuous_re.comp (l i).continuous) continuous_const)
  exact ⟨l ∘ k, c ∘ k, hk.trans this⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
⊢ ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)

Tactic:
by
  apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
  · intro e s s_meas _
    rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ.real s) e,
      map_smulₛₗ, hσ, map_one, smul_assoc, one_smul,
      ← integral_indicator_const (L e) s_meas]
    congr 1 with a
    rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]
  · intro f g _ f_int g_int hf hg
    simp [L.map_add, integral_add (μ := μ) f_int g_int,
      integral_add (μ := μ) (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg]
  · exact isClosed_eq L.continuous_integral_comp_L1 (L.continuous.comp continuous_integral)
  · intro f g hfg _ hf
    convert! hf using 1 <;> clear hf
    · exact integral_congr_ae (hfg.fun_comp L).symm
    · rw [integral_congr_ae hfg.symm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_8
inst✝² : Fintype ι
M : ι → Type u_9
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

Tactic:
by_cases! hm : ∀ i, m i ≠ 0

Goal state after:
case pos
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_8
inst✝² : Fintype ι
M : ι → Type u_9
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∀ (i : ι), m i ≠ 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ

case neg
X : Type u_1
E : Type u_3
inst✝⁷ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace ℝ E
ι : Type u_8
inst✝² : Fintype ι
M : ι → Type u_9
inst✝¹ : (i : ι) → NormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
φ : X → ContinuousMultilinearMap 𝕜 M E
φ_int : Integrable φ μ
m : (i : ι) → M i
hE : ¬CompleteSpace E
hm : ∃ i, m i = 0
⊢ (∫ (x : X), φ x ∂μ) m = ∫ (x : X), (φ x) m ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
integral_undef hg,

Goal state after:
case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ 0 = ∫ (x : X), f x • g x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ (∫ (x : X), g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
rw [integral_undef hg, integral_undef]

Goal state after:
case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : ¬Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ ¬Integrable (fun x ↦ f x • g x) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
⊢ (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ →
    (∫ (x : X), v x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • v x ∂μ

Tactic:
hu

Goal state after:
case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
⊢ (∫ (x : X), v x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • v x ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
⊢ (∫ (a : X), u a ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • v x ∂μ

Tactic:
hu

Goal state after:
case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
⊢ ∫ (x : X), f x • u x ∂μ = ∫ (x : X), f x • v x ∂μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : μ {b₀} = 0
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ EqOn (fun b ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) (fun b ↦ ∫ (x : ℝ) in b₁..b₂, {x | x ≤ b}.indicator f x ∂μ) (Icc b₁ b₂)

Tactic:
exact fun b b_in => (integral_indicator b_in).symm

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this✝¹ : MeasurableSpace F := ⋯
this✝ : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ Ici x ⊆ closure (Ici x ∩ t)

Tactic:
calc Ici x
    = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
  _ ⊆ closure (closure (Ioi x ∩ t)) := by
      apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
  _ ⊆ closure (Ici x ∩ t) := by
      rw [closure_closure]
      exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
⊢ u ∈ Ioo t (min M b) → (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal

Tactic:
hu

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
⊢ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c = 0
⊢ c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
simp [hc, integral_comp_mul_right]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case neg
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
hc : ¬c = 0
⊢ c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
simp [hc, integral_comp_mul_right]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < ↑∞
hx : x ∈ Icc t u
⊢ y ≤ (G' x).toReal

Tactic:
apply EReal.coe_le_coe_iff.1

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := ⋯
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < ↑∞
hx : x ∈ Icc t u
⊢ ↑y ≤ ↑(G' x).toReal
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
u : ℝ
⊢ slope g t u < y → u ∈ Ioi t → g u - g t ≤ (u - t) * y

Tactic:
hu

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
⊢ u ∈ Ioi t → g u - g t ≤ (u - t) * y
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
have : ∀ x ∈ Icc a b, ∫ t in Ioc a x, f t ∂μ = ∫ t in a..x, f t ∂μ := by
      intro x x_in
      simp_rw [integral_of_le x_in.1]
    rw [continuousOn_congr this]
    intro x₀ _
    refine continuousWithinAt_primitive (measure_singleton x₀) ?_
    simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self]
    exact h_int.mono Ioc_subset_Icc_self le_rfl

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hsub : [[c, d]] ⊆ k
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False

Tactic:
have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ :=
    (ae_restrict_mem measurableSet_uIoc).mono hg

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd✝ : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hsub : [[c, d]] ⊆ k
hd : d ∈ s
hlt : ‖f c‖ + ∫ (y : ℝ) in k, C * ‖g y‖ < ‖f d‖
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
⊢ False
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_3
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn (fun t ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : ℝ → 𝕜 := fun t ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0

Tactic:
· simp only [γ, Function.comp_apply, one_smul, zero_smul, add_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0

Tactic:
by
  rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
    MeasureTheory.integral_pos_iff_support_of_nonneg_ae]

Goal state after:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < (μ.restrict (Ioc a b)) (support fun x ↦ g x - f x)

case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᵐ[μ.restrict (Ioc a b)] fun x ↦ g x - f x

case hfi
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable (fun x ↦ g x - f x) (μ.restrict (Ioc a b))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ IntervalIntegrable f volume (a k) (a (k + 1))

Tactic:
convert! (IntervalIntegrable.comp_sub_right h₂f ((k - n₁) * T) enorm_ne_top) using 1

Goal state after:
case e'_4
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ f = fun x ↦ f (x - (↑k - ↑n₁) * T)

case e'_7
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume t (t + T)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ a (k + 1) = t + T + (↑k - ↑n₁) * T
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)

Tactic:
by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]

Goal state after: