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

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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬x = ↑(extChartAt I x).symm z

Tactic:
(extChartAt I x).eq_symm_apply (by simp) hz.2

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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬↑(extChartAt I x) x = z
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))
hg :
  ContinuousWithinAt g u (f x) ∧
    HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g) g' (↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑(extChartAt I x) x))
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) (↑(extChartAt I x) x)
hst : s ⊆ f ⁻¹' u
this✝¹ :
  ↑(extChartAt I x).symm ⁻¹' f ⁻¹' (extChartAt I' (f x)).source ∈
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
this✝ : writtenInExtChartAt I I' x f (↑(extChartAt I x) x) = ↑(extChartAt I' (f x)) (f x)
y : E
hy :
  (↑(chartAt H x).symm (↑I.symm y) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm y)) ∈ (chartAt H' (f x)).source) ∧ y ∈ range ↑I
this : f (↑(chartAt H x).symm (↑I.symm y)) ∈ u
⊢ writtenInExtChartAt I I' x f y ∈ ↑(extChartAt I' (f x)).symm ⁻¹' u ∩ range ↑I'

Tactic:
simp only [hy, this, mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case h₁
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : TopologicalSpace (TotalSpace F E)
inst✝⁷ : (x : B) → TopologicalSpace (E x)
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✝¹ : FiberBundle F E
s : (x : B) → E x
u : Set B
x : B
inst✝ : Subsingleton F
⊢ ∀ y ∈ u, (↑(trivializationAt F E x) { proj := y, snd := s y }).2 = ?m.113

Tactic:
intro y _

Goal state after:
case h₁
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : TopologicalSpace (TotalSpace F E)
inst✝⁷ : (x : B) → TopologicalSpace (E x)
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✝¹ : FiberBundle F E
s : (x : B) → E x
u : Set B
x : B
inst✝ : Subsingleton F
y : B
a✝ : y ∈ u
⊢ (↑(trivializationAt F E x) { proj := y, snd := s y }).2 = ?m.113
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈
    (tangentBundleCore I M).baseSet (achart H w) ∩ (tangentBundleCore I M).baseSet (achart H x) ∩
      (tangentBundleCore I M).baseSet (achart H y)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
w x y z : M
v : E
h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
⊢ z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
⊢ (extChartAt I x).source = (tangentBundleCore I M).baseSet (achart H x)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case e'_4
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
⊢ (extChartAt I y).source = (tangentBundleCore I M).baseSet (achart H y)

Tactic:
simp only [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: case ofNat
𝕜 : 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 : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ ⇑(Int.ofNat n • s) = Int.ofNat n • ⇑s

Tactic:
refine (coe_nsmul s n).trans ?_
    simp only [Int.ofNat_eq_natCast, natCast_zsmul]

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), { toFun := f.toPOUFun i, continuous_toFun := ⋯ } x ≤ 1

Tactic:
by
    simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]
    exact finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
⊢ ∃ ι f, f.IsSubordinate U

Tactic:
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
    ⟨ι, c, f, hf, hsub', hfin⟩

Goal state after:
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hf : ∀ (a : ι), c a ∈ s ∧ tsupport ↑(f a) ⊆ U (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
⊢ ∃ ι f, f.IsSubordinate U
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
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
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := eball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), n + k + 1 ≤ m → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : eball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ edist z z' + edist z x + (edist y x + edist y y') < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m)

Tactic:
by
          apply_rules [ENNReal.add_lt_add]

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

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

Tactic:
by
  refine ae_nonneg_of_forall_setIntegral_nonneg hf fun s hs h's => ?_
  simp_rw [Measure.restrict_restrict hs]
  apply hf_zero s hs
  rwa [Measure.restrict_apply hs] at h's

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
by
  have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
  have : FiniteDimensional 𝕜 F := .of_locallyCompactSpace 𝕜
  have : ProperSpace E := .of_locallyCompactSpace 𝕜
  have : ProperSpace F := .of_locallyCompactSpace 𝕜
  let M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
  have M_cont : Continuous M := M.continuous_of_finiteDimensional
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `range_eq_top` into
  -- `range_eq_top (f := _)`
  have hM : Function.Surjective M := by
    simp [M, ← LinearMap.range_eq_top (f := _), LinearMap.range_coprod]
  have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.rfl
  simp_rw [← ae_comp_linearMap_mem_iff M (ν.prod μ) ν hM hs, A]
  rw [Measure.ae_prod_mem_iff_ae_ae_mem]
  · simp only [M, mem_preimage, LinearMap.coprod_apply, LinearMap.id_coe, id_eq]
  · exact M_cont.measurable hs

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ tᶜ
⊢ x ∈ t

Tactic:
by simpa using xs

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommGroup (E i)
inst✝³ : (i : ι) → Module 𝕜 (E i)
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi s) x

Tactic:
simp only [uniqueDiffWithinAt_iff, closure_pi_set] at h ⊢

Goal state after:
𝕜 : Type u_1
inst✝⁵ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommGroup (E i)
inst✝³ : (i : ι) → Module 𝕜 (E i)
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure[inst✝² i] (s i)
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x)) ∧ x ∈ univ.pi fun i ↦ closure[inst✝² i] (s i)
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 D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
⊢ ∫ (x : E), (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ

Tactic:
have S3 : ∫ x, f (x + t • v) * g x ∂μ = ∫ x, f x * g (x + t • (-v)) ∂μ := by
    rw [← integral_add_right_eq_self _ (t • (-v))]; simp

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
S3 : ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ
⊢ ∫ (x : E), (f (x + t • v) - f x) * g x ∂μ = ∫ (x : E), f x * (g (x + t • -v) - g x) ∂μ
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0) f s
hf' : DifferentiableWithinAt ℝ f s y
⊢ HasDerivWithinAt (fun t ↦ f t) (derivWithin f s y) s' y

Tactic:
exact hf'.hasDerivWithinAt.mono h

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
hu₄ : Tendsto (fun s ↦ ∑ b ∈ s, dist (f (↑b).1) (f (↑b).2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
⊢ dist (f d) (f b) ≤ y

Tactic:
u_coe_sum _ fun x y ↦ dist (f x) (f y)

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
⊢ dist (f d) (f b) ≤ y
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (deriv fun t ↦ (x - t) ^ k / ↑k !) MeasureTheory.volume x₀ x

Tactic:
apply ContinuousOn.intervalIntegrable

Goal state after:
case inr.hu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ContinuousOn (deriv fun t ↦ (x - t) ^ k / ↑k !) [[x₀, x]]
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hv'.h
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] =ᵐ[MeasureTheory.volume.restrict (Ι x₀ x)]
    deriv fun t ↦ iteratedDerivWithin k f [[x₀, x]] t

Tactic:
rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by measurability)]

Goal state after:
case inr.hv'.h
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this✝ : f a = g a
this : g a = C
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
have := hC b (by simp)

Goal state after:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
this✝¹ : f a = g a
this✝ : g a = C
this : g b = C
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
have :=
    combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x)
      (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy) (div_pos hy hxy)
      (by rw [← add_div, div_self hxy.ne'])

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : (‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y ∈ ball 0 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x ↦ deriv (fun a ↦ a ^ n) x

Tactic:
deriv_pow_field

Goal state after:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x ↦ ↑n * x ^ (n - 1)