mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝¹¹] a
ha' : a ⊆ e.baseSet
⊢ ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a ↔
    ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;>
  have := (h x hx).contMDiffAt <| ha.mem_nhds hx

Goal state after:
case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝¹¹] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a
x : B
hx : x ∈ a
this : ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x
⊢ ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a x

case refine_2
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝¹¹] a
ha' : a ⊆ e.baseSet
h : ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a
x : B
hx : x ∈ a
this : ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) x
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝³⁸ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝³⁷ : NormedAddCommGroup EB
inst✝³⁶ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³⁵ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝³⁴ : TopologicalSpace B
inst✝³³ : ChartedSpace HB B
EM : Type u_9
inst✝³² : NormedAddCommGroup EM
inst✝³¹ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝³⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝²⁹ : TopologicalSpace M
inst✝²⁸ : ChartedSpace HM M
inst✝²⁷ : (x : B) → AddCommMonoid (E x)
inst✝²⁶ : (x : B) → Module 𝕜 (E x)
inst✝²⁵ : NormedAddCommGroup F
inst✝²⁴ : NormedSpace 𝕜 F
inst✝²³ : TopologicalSpace (TotalSpace F E)
inst✝²² : (x : B) → TopologicalSpace (E x)
inst✝²¹ : FiberBundle F E
inst✝²⁰ : VectorBundle 𝕜 F E
inst✝¹⁹ : ContMDiffVectorBundle n F E IB
F₁ : Type u_11
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜 F₁
E₁ : B → Type u_12
inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹⁵ : (x : B) → AddCommMonoid (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
F₂ : Type u_13
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜 F₂
E₂ : B → Type u_14
inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁰ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : VectorBundle 𝕜 F₂ E₂
inst✝² : ContMDiffVectorBundle n F₁ E₁ IB
inst✝¹ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝ : IsManifold IB n B
⊢ ∀ (e e' : Trivialization (F₁ × F₂) TotalSpace.proj) [inst : MemTrivializationAtlas e]
    [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₁ × F₂) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b))
      (e.baseSet ∩ e'.baseSet)

Tactic:
by
    rintro _ _ ⟨e₁, e₂, i₁, i₂, rfl⟩ ⟨e₁', e₂', i₁', i₂', rfl⟩
    refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')
    refine ContMDiffOn.clm_prodMap ?_ ?_
    · refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_
      simp only [Trivialization.prod_baseSet, mfld_simps]
      mfld_set_tac
    · refine (contMDiffOn_coordChangeL e₂ e₂').mono ?_
      simp only [Trivialization.prod_baseSet, mfld_simps]
      mfld_set_tac

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
⊢ ParacompactSpace α

Tactic:
have hpow_le : ∀ {m n : ℕ}, m ≤ n → (2⁻¹ : ℝ≥0∞) ^ n ≤ 2⁻¹ ^ m := @fun m n h =>
    pow_le_pow_right_of_le_one' (ENNReal.inv_le_one.2 ENNReal.one_lt_two.le) h

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
⊢ ParacompactSpace α
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
⊢ ∃ β t,
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
set D : ℕ → ι → Set α :=
    Nat.strongRec fun n D' i ↦
      ⋃ (x : α) (hxs : ind x = i) (hb : eball x (3 * 2⁻¹ ^ n) ⊆ s i) (hlt :
        ∀ (m : ℕ) (H : m < n), ∀ (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n) with hD

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
⊢ ∃ β t,
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u x₀
ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (s + t) x⟩) u x₀

Tactic:
contMDiffWithinAt_section

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, t x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, (s + t) x⟩).2) u x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (-s) x⟩) u x₀

Tactic:
contMDiffWithinAt_section

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, (-s) x⟩).2) u x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (f • s) x⟩) u x₀

Tactic:
contMDiffWithinAt_section

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F V x₀) ⟨x, (f • s) x⟩).2) u x₀
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport x₀ ⊆ I
⊢ ∑ i ∈ I, (ρ i) x₀ = 1

Tactic:
by
  classical
  rw [← Finset.sum_sdiff hI, ρ.sum_finsupport hx₀]
  suffices ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0 by
    rw [this, add_eq_right, Finset.sum_const_zero]
  apply Finset.sum_congr rfl
  rintro x hx
  simp only [Finset.mem_sdiff, ρ.mem_finsupport, mem_support, Classical.not_not] at hx
  exact hx.2

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ 0 ≤ᵐ[μ] f

Tactic:
simp_rw [EventuallyLE, Pi.zero_apply]
  rw [ae_const_le_iff_forall_lt_measure_zero]
  intro b hb_neg
  let s := {x | f x ≤ b}
  have hs : NullMeasurableSet s μ := nullMeasurableSet_le hf.1.aemeasurable aemeasurable_const
  have mus : μ s < ∞ := Integrable.measure_le_lt_top hf hb_neg
  have h_int_gt : (∫ x in s, f x ∂μ) ≤ b * μ.real s := by
    have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
      refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_
      rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
      exact Eventually.of_forall fun x hxs => hxs
    rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
  contrapose! h_int_gt with H
  calc
    b * μ.real s < 0 := mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne
    _ ≤ ∫ x in s, f x ∂μ := by
      rw [← μ.restrict_toMeasurable mus.ne]
      exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])

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

Goal state before:
pp: case hF_meas
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (fun a ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ

Tactic:
apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (fun a ↦ t⁻¹ • (f (a + t • v) - f a)) μ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 0

Tactic:
exact hf_zero _ (hs.inter hf.measurableSet) hμs

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

Goal state before:
pp: case hF_meas
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (fun a ↦ t⁻¹ • (f (a + t • v) - f a) * g a) μ

Tactic:
apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (fun a ↦ t⁻¹ • (f (a + t • v) - f a)) μ
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
refine ⟨l, ?_, ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ tangentConeAt 𝕜 s x

case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ {0}ᶜ
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S2 : ∫ (x : E), (∑ i ∈ s, a i * (fderiv ℝ g x) (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), (fderiv ℝ g x) (v i) * f x ∂μ
D : ℝ≥0
g_lip : LipschitzWith D g
⊢ ∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ

Tactic:
simp_rw [integral_lineDeriv_mul_eq hf g_lip g_comp]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S2 : ∫ (x : E), (∑ i ∈ s, a i * (fderiv ℝ g x) (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), (fderiv ℝ g x) (v i) * f x ∂μ
D : ℝ≥0
g_lip : LipschitzWith D g
⊢ ∫ (x : E), lineDeriv ℝ g x (-∑ i ∈ s, a i • v i) * f x ∂μ =
    ∑ x ∈ s, a x * ∫ (x_1 : E), lineDeriv ℝ g x_1 (-v x) * f x_1 ∂μ
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
⊢ HasFDerivAt f L x

Tactic:
hasFDerivAt_iff_isLittleO_nhds_zero,

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
⊢ (fun h ↦ f (x + h) - f x - L h) =o[𝓝 0] fun h ↦ h
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f • g) a b

Tactic:
obtain ⟨C, hC⟩ := hf.exists_bound

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
⊢ AbsolutelyContinuousOnInterval (f • g) a b