mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / (12 * ‖c‖)
e' : ℕ
he' : e' ≥ e
⊢ dist (L0 e') (L0 e) < ε

Tactic:
rw [dist_comm, dist_eq_norm]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →L[𝕜] F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ),
    n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / (12 * ‖c‖)
e' : ℕ
he' : e' ≥ e
⊢ ‖L0 e - L0 e'‖ < ε
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
⊢ gauge s (-x) = gauge s x

Tactic:
by
  have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩
  simp_rw [gauge_def', smul_neg, this]

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε =
    ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2 + (∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2)

Tactic:
conv_lhs => rw [← ENNReal.add_halves ε]

Goal state after:
case e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + (ε / 2 + ε / 2) =
    ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2 + (∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
x✝² : { c // 0 ≤ c }
x✝¹ : E × ℝ
x✝ : x✝¹ ∈ {p | N p.1 ≤ p.2}
val✝ : ℝ
hc : 0 ≤ val✝
⊢ ⟨val✝, hc⟩ • x✝¹ ∈ {p | N p.1 ≤ p.2}

Tactic:
by rcases eq_or_lt_of_le' hc <;> simp_all

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

Goal state before:
pp: E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
α : Type u_3
inst✝⁸ : Field α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : MulActionWithZero α ℝ
inst✝⁴ : IsStrictOrderedModule α ℝ
inst✝³ : Module α E
inst✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
⊢ gauge (a • s) = |a|⁻¹ • gauge s

Tactic:
by
  rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]
  obtain h | h := abs_choice a
  · rw [h]
  · rw [h, Set.neg_smul_set, ← Set.smul_set_neg]
    congr
    ext y
    refine ⟨symmetric _, fun hy => ?_⟩
    rw [← neg_neg y]
    exact symmetric _ hy

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s t : Set E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
hzero : StrongDual.extendRCLikeₗ f = 0
⊢ False

Tactic:
exact hfne <| (StrongDual.extendRCLikeₗ (𝕜 := 𝕜)).injective (by simpa using hzero)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_1
𝕜 : 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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, f a ≤ f x
hzero : StrongDual.extendRCLikeₗ f = 0
⊢ False

Tactic:
exact hfne <| (StrongDual.extendRCLikeₗ (𝕜 := 𝕜)).injective (by simpa using hzero)

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 ι
g : ℕ → ContinuousMultilinearMap 𝕜 M F :=
  fun n ↦
    (compContinuousLinearMapL φ) (((smulRightL 𝕜 (fun x ↦ 𝕜) F) (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))
this : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
⊢ Tendsto f atTop (𝓝 (a m))

Tactic:
have : Tendsto (fun n ↦ g n m) atTop (𝓝 (a m)) := ((continuous_eval_const _).tendsto _).comp ha

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))
this✝ : CauchySeq g
a : ContinuousMultilinearMap 𝕜 M F
ha : Tendsto g atTop (𝓝 a)
this : Tendsto (fun n ↦ (g n) m) atTop (𝓝 (a m))
⊢ Tendsto f atTop (𝓝 (a m))
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε

Tactic:
by
  have := hx.hasDerivWithinAt
  simp_rw [hasDerivWithinAt_iff_isLittleO, isLittleO_iff] at this
  rcases mem_nhdsGE_iff_exists_Ico_subset.1 (this (half_pos hε)) with ⟨m, xm, hm⟩
  refine ⟨m - x, by linarith [show x < m from xm], fun r hr => ?_⟩
  have : r ∈ Ioc (r / 2) r := ⟨half_lt_self hr.1, le_rfl⟩
  refine ⟨r, this, fun y hy z hz => ?_⟩
  calc
    ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x -
            (f y - f x - (y - x) • derivWithin f (Ici x) x)‖ := by
      congr 1; simp only [sub_smul]; abel
    _ ≤
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x‖ +
          ‖f y - f x - (y - x) • derivWithin f (Ici x) x‖ :=
      (norm_sub_le _ _)
    _ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
      (add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩)
        (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
    _ ≤ ε / 2 * r + ε / 2 * r := by
      gcongr
      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
    _ = ε * r := by ring

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ (mkD (s.domRestrict f) g) x = f ↑x

Tactic:
mkD_of_continuousOn hf hf₀,

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ { toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf₀ } x = f ↑x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: 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
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ

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
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ

Tactic:
· exact ((ContinuousLinearMap.apply 𝕜 E v).integral_comp_comm φ_int).symm

Goal state after:
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
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
φ : X → H →L[𝕜] E
φ_int : Integrable φ μ
v : H
hE : ¬CompleteSpace E
⊢ (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / 12
e' : ℕ
he' : e' ≥ e
⊢ dist (L0 e') (L0 e) < ε

Tactic:
rw [dist_comm, dist_eq_norm]

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun e ↦ L e (n e) (n e)
ε : ℝ
εpos : ε > 0
e : ℕ
he : (1 / 2) ^ e < ε / 12
e' : ℕ
he' : e' ≥ e
⊢ ‖L0 e - L0 e'‖ < ε
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_1.hfi
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))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x ↦ ↑(f x)) s < ∞
⊢ Integrable (fun x ↦ ↑(f x)) (μ.restrict s)

Tactic:
· refine ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩
      simpa [withDensity_apply _ s_meas, hasFiniteIntegral_iff_enorm] using hs

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

Goal state before:
pp: case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
⊢ IntegrableOn (fun x ↦ f (c * x)) [[a / c, b / c]] volume

Tactic:
have A : MeasurableEmbedding fun x => x * c⁻¹ :=
    (Homeomorph.mulRight₀ _ (inv_ne_zero hc)).isClosedEmbedding.measurableEmbedding

Goal state after:
case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding fun x ↦ x * c⁻¹
⊢ IntegrableOn (fun x ↦ f (c * x)) [[a / c, b / c]] volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a✝ b✝ : ℝ
inst✝ : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding fun x ↦ x + c
⊢ IntegrableOn (fun x ↦ f (x + c)) [[a - c, b - c]] volume

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a✝ b✝ : ℝ
inst✝ : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn f [[a, b]] (Measure.map (fun x ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding fun x ↦ x + c
⊢ IntegrableOn (fun x ↦ f (x + c)) [[a - c, b - c]] volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝⁴ : NormedAddCommGroup E
μ : Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntervalIntegrable u μ a b

Tactic:
rw [intervalIntegrable_iff]
  exact (hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
⊢ (range fun p ↦ deriv (f p.1) p.2) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (range (Function.uncurry f)))

Tactic:
rintro - ⟨p, rfl⟩

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
⊢ (fun p ↦ deriv (f p.1) p.2) p ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (range (Function.uncurry f)))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
integral_Iio_sub_Iio hf hab,

Goal state after:
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a✝ b✝ : ℝ
f : ℝ → E
μ : Measure ℝ
inst✝ : NullSingletonClass μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ico a b, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: 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 ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
⊢ QuotientMeasureEqMeasurePreimage ν (c • haarMeasure K)

Tactic:
have c_ne_top : c ≠ ∞ := measure_inter_ne_top_of_right_ne_top h𝓕_finite

Goal state after:
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 ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕)
c_ne_top : c ≠ ∞
⊢ QuotientMeasureEqMeasurePreimage ν (c • haarMeasure K)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ deriv (circleMap c R) θ = 0 ↔ R = 0

Tactic:
simp [I_ne_zero]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ (fun θ ↦ f₁ (circleMap c R θ)) =ᶠ[codiscreteWithin (Ι 0 (2 * π))] fun θ ↦ f₂ (circleMap c R θ)

Tactic:
eventuallyEq_iff_exists_mem

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f₁ f₂ : ℂ → E
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hf₁ : CircleIntegrable f₁ c R
hR : ¬R = 0
⊢ ∃ s ∈ codiscreteWithin (Ι 0 (2 * π)), EqOn (fun θ ↦ f₁ (circleMap c R θ)) (fun θ ↦ f₂ (circleMap c R θ)) s
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
hne : ¬∃ i, a i = b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Tactic:
have hlt : ∀ i, a i < b i := fun i => (hle i).lt_of_ne fun hi => hne ⟨i, hi⟩

Goal state after:
case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
a b : Fin (n + 1) → ℝ
hle : a ≤ b
f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ (Set.univ.pi fun i ↦ Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun x ↦ ∑ i, (f' x) (e i) i) (Set.Icc a b) volume
hne : ¬∃ i, a i = b i
hlt : ∀ (i : Fin (n + 1)), a i < b i
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (e i) i =
    ∑ i,
      ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
        ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)
Module: Mathlib.Topology.Maps.Proper.CompactlyGenerated

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : CompactlyCoherentSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ Tendsto f (cocompact X) (cocompact Y)

Tactic:
simp_rw [isProperMap_iff_isCompact_preimage,
    hasBasis_cocompact.tendsto_right_iff, ← mem_preimage, eventually_mem_set, preimage_compl]
  refine and_congr_right fun f_cont ↦
    ⟨fun H K hK ↦ (H hK).compl_mem_cocompact, fun H K hK ↦ ?_⟩
  rcases mem_cocompact.mp (H K hK) with ⟨K', hK', hK'y⟩
  exact hK'.of_isClosed_subset (hK.isClosed.preimage f_cont)
    (compl_le_compl_iff_le.mp hK'y)

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a))) l atTop

Tactic:
refine .atTop_of_add_const (abv (-f a)) ?_

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < p✝.degree
ihp : f p✝.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p✝)) l atTop
hf : f p✝.leadingCoeff ≠ 0
⊢ Tendsto (fun x ↦ abv (eval₂ f (z x) (p✝ + C a)) + abv (-f a)) l atTop