mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (⇑f) (f.linear 1) L

Tactic:
rw [f.decomp]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (⇑f.linear + fun x ↦ f 0) (f.linear 1) L
Module: Mathlib.Analysis.Calculus.ContDiff.RCLike

Goal state before:
pp: n : ℕ∞ω
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : n ≠ 0
⊢ ∃ C, LipschitzWith C f

Tactic:
obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)
  refine ⟨.mk (max C 0) (le_max_right _ _), ?_⟩
  apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)
  simp [← NNReal.coe_le_coe, hC x]

Goal state after:
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
⊢ logDeriv (fun x ↦ f x ^ n) x = ↑n * logDeriv f x

Tactic:
rcases eq_or_ne n 0 with rfl | hn; · simp
  rcases eq_or_ne (f x) 0 with hf | hf
  · simp [logDeriv_apply, zero_zpow, *]
  · rw [logDeriv_apply, ← comp_def (· ^ n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
      deriv_zpow, logDeriv_apply]
    simp [field, zpow_sub_one₀ hf]

Goal state after:
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ f x = f y

Tactic:
exact convex_univ.is_const_of_fderivWithin_eq_zero hf.differentiableOn
    (fun x _ => by rw [fderivWithin_univ]; exact hf' x) trivial trivial

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOnNhd 𝕜 (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun x ↦ E) F G) g)) univ

Tactic:
exact ContinuousLinearMap.analyticOnNhd _ _

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Deriv

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : 𝕜 → F
h : ContDiff 𝕜 n f
hn : 1 ≤ n
⊢ Continuous (deriv f)

Tactic:
rw [show (1 : ℕ∞ω) = 0 + 1 from rfl] at hn
  exact (contDiff_succ_iff_deriv.mp (h.of_le hn)).2.2.continuous

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ContDiffWithinAt 𝕜 m (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
rw [← insert_eq_self.mpr hx₀] at hf
  refine hf.fderivWithin' hg ?_ hmn hst
  rw [insert_eq_self.mpr hx₀]
  exact eventually_of_mem self_mem_nhdsWithin fun x hx => ht _ (hst hx)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
A : ∀ (m : ℕ), ↑m ≤ n → ContDiffWithinAt 𝕜 (↑m) (fun y ↦ fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 n (fderivWithin 𝕜 f s) s x

Tactic:
match n with
  | ω => exact (H.analyticOn.fderivWithin hs).contDiffOn hs (n := ω) x hx
  | ∞ => exact contDiffWithinAt_infty.2 (fun m ↦ A m (mod_cast le_top))
  | (n : ℕ) => exact A n le_rfl

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

Goal state before:
pp: 𝕂 : Type u_1
inst✝² : NontriviallyNormedField 𝕂
inst✝¹ : CompleteSpace 𝕂
inst✝ : CharZero 𝕂
x : 𝕂
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝕂).radius
⊢ HasStrictDerivAt exp (exp x) x

Tactic:
simpa using (hasStrictFDerivAt_exp_of_mem_ball hx).hasStrictDerivAt

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

Goal state before:
pp: 𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 0)

Tactic:
← zero_smul 𝕊 x

Goal state after:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕂
inst✝⁸ : CharZero 𝕂
inst✝⁷ : NormedCommRing 𝕊
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedSpace 𝕂 𝕊
inst✝⁴ : NormedAlgebra 𝕂 𝔸
inst✝³ : Algebra 𝕊 𝔸
inst✝² : ContinuousSMul 𝕊 𝔸
inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx : t • x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ Tendsto (fun h ↦ h • x) (𝓝 0) (𝓝 (0 • x))
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (fun x ↦ f x - g x) x

Tactic:
by simpa only [sub_eq_add_neg] using hf.add hg.neg

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n fun x ↦ f x - g x

Tactic:
by simpa only [sub_eq_add_neg] using hf.add hg.neg

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' : ∀ (i : ℕ), AnalyticOn 𝕜' (fun x ↦ p' x i) u
i : ℕ
⊢ AnalyticOnNhd 𝕜 (⇑(ContinuousMultilinearMap.restrictScalarsLinear 𝕜)) univ

Tactic:
exact ContinuousLinearMap.analyticOnNhd _ _

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
⊢ ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε

Tactic:
rcases exists_le_lowerSemicontinuous_lintegral_ge μ (s.indicator fun _x => ∞)
      (measurable_const.indicator smeas) this with
    ⟨g1, le_g1, g1_cont, g1_int⟩

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
⊢ ∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : ConvexCone R M
h : C.IsReproducing
⊢ Submodule.span R ↑C = ⊤

Tactic:
rw [eq_top_iff]
  rintro x -
  rw [IsReproducing, Set.eq_univ_iff_forall] at h
  obtain ⟨y, hy, z, hz, rfl⟩ := Set.mem_sub.mp (h x)
  exact sub_mem (Submodule.subset_span hy) (Submodule.subset_span hz)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
x : M
hs : Convex 𝕜 s
hx : x ∈ hull 𝕜 s
⊢ ∀ ⦃x : M⦄,
    x ∈ {y | ∃ r, 0 < r ∧ y ∈ r • s} →
      ∀ ⦃y : M⦄, y ∈ {y | ∃ r, 0 < r ∧ y ∈ r • s} → x + y ∈ {y | ∃ r, 0 < r ∧ y ∈ r • s}

Tactic:
by
                rintro y₁ ⟨r₁, hr₁, hy₁⟩ y₂ ⟨r₂, hr₂, hy₂⟩
                refine ⟨r₁ + r₂, add_pos hr₁ hr₂, ?_⟩
                rw [hs.add_smul hr₁.le hr₂.le]
                exact add_mem_add hy₁ hy₂

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
c : 𝕜
hc : 0 < c
hcx : c • x ∈ s
⊢ c⁻¹ • c • x = x

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
⊢ False

Tactic:
have hpx : 0 < p x := (apply_nonneg _ _).lt_of_ne h

Goal state after:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
⊢ False
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : TopologicalSpace V
inst✝² : TopologicalSpace R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
h : ∀ (f : StrongDual R V), f x = 0
hx : ¬x = 0
f : StrongDual R V
hf : f x ≠ 0
⊢ False

Tactic:
exact hf (h f)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain

Goal state before:
pp: case intro
𝕜 : Type u_1
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_4
inst✝⁴ : Finite ι
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual 𝕜 (M i)
hφ : ∀ (i : ι), (φ i) (m i) = 1
val✝ : Fintype ι
⊢ ∃ a, Tendsto f atTop (𝓝 a)

Tactic:
let g : ℕ → (ContinuousMultilinearMap 𝕜 M F) := fun n ↦
    compContinuousLinearMapL φ
    (ContinuousMultilinearMap.smulRightL 𝕜 _ F ((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))

Goal state after:
case intro
𝕜 : Type u_1
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
ι : Type u_4
inst✝⁴ : Finite ι
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
inst✝¹ : ∀ (i : ι), SeparatingDual 𝕜 (M i)
inst✝ : CompleteSpace (ContinuousMultilinearMap 𝕜 M F)
m : (i : ι) → M i
hm : ∀ (i : ι), m i ≠ 0
f : ℕ → F
hf : CauchySeq f
φ : (i : ι) → StrongDual 𝕜 (M i)
hφ : ∀ (i : ι), (φ i) (m i) = 1
val✝ : Fintype ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun n ↦
    (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x ↦ 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))
⊢ ∃ a, Tendsto f atTop (𝓝 a)
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
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
⊢ ∃ f, f ≠ 0 ∧ ∀ a ∈ A, re (f a) ≤ re (f x)

Tactic:
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨f, hfne, hA'⟩ := _root_.geometric_hahn_banach_of_nonempty_interior_point hA hxA hAint
  refine ⟨f.extendRCLikeₗ, fun hzero ↦ ?_, ?_⟩
  · exact hfne <| (StrongDual.extendRCLikeₗ (𝕜 := 𝕜)).injective (by simpa using hzero)
  · simpa [f.extendRCLikeₗ_apply] using hA'

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
μ : Measure X
A : Type u_8
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c

Tactic:
by
  by_cases hA : CompleteSpace A
  · change ∫ x, (ContinuousLinearMap.mul ℝ _).flip c (f x) ∂μ
      = (ContinuousLinearMap.mul ℝ _).flip c (∫ x, f x ∂μ)
    rw [ContinuousLinearMap.integral_comp_comm _ hf]
  · simp [integral, hA]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

Tactic:
rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
⊢ (fun t ↦
      ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
        (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
    fun t ↦ ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖

Tactic:
have := FTCFilter.meas_gen la

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this : la'.IsMeasurablyGenerated
⊢ (fun t ↦
      ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
        (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
    fun t ↦ ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ 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 <;> simp [hc, integral_comp_mul_add]

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0

Tactic:
have hac := hab.trans hbc
  simp only [intervalIntegral, sub_add_sub_comm, sub_eq_zero]
  iterate 4 rw [← setIntegral_union]
  · suffices Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c by rw [this]
    rw [Ioc_union_Ioc_union_Ioc_cycle, union_right_comm, Ioc_union_Ioc_union_Ioc_cycle,
      min_left_comm, max_left_comm]
  all_goals
    simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

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

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

Tactic:
integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᵐ[μ.restrict (Ioc b a)] f
⊢ f =ᵐ[μ.restrict (Ioc b a)] 0 ↔ f =ᵐ[μ.restrict (Ioc b a)] 0
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
t : α
ht : ¬∃ n, t = ↑n
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, t)

Tactic:
replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
    refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))
    exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case neZeroV.a
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
V : Set (G ⧸ Γ)
hV : (interior V).Nonempty
meas_V : MeasurableSet V
hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)
neTopV : μ V ≠ ∞
c_eq_zero : ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕) = 0
⊢ ν (interior (QuotientGroup.mk ⁻¹' V)) = 0

Tactic:
· apply measure_mono_null (h := interior_subset)
      apply h𝓕.measure_zero_of_invariant (ht := fun g ↦ QuotientGroup.sound _ _ g)
      exact c_eq_zero

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case bound_integrable
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ Integrable ((Ioi a₀).indicator (norm ∘ f)) μ

pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))

Tactic:
· simpa [integrable_indicator_iff measurableSet_Ioi] using! hf.norm

Goal state after:
case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun n ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h_lim
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
⊢ Tendsto (fun n ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))

Tactic:
by_cases hx : x < a₀

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
⊢ Tendsto (fun n ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
⊢ Tendsto (fun n ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a

Tactic:
have h_split : ∀ b ∈ Icc a a₀, ∫ x in Iio b, f x ∂μ =
        (∫ x in Iio a₀, f x ∂μ) + ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [integral_symm b a₀, ← integral_Iio_sub_Iio' hf (hf.mono_set (Iio_subset_Iio hb.2))]

Goal state after:
case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ≤ a₀
h_int : IntervalIntegrable f μ a a₀
h_split : ∀ b ∈ Icc a a₀, ∫ (x : ℝ) in Iio b, f x ∂μ = ∫ (x : ℝ) in Iio a₀, f x ∂μ + ∫ (x : ℝ) in a₀..b, f x ∂μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Icc a a₀) a