mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1

Tactic:
· use i
      rw [update_self]
      exact hvi ⟨hx, mem_biInter h⟩

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
hj : j ∈ v.carrier
⊢ closure (v.toFun j) ⊆ u j

Tactic:
exact v.closure_subset hj

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
i : ι
s : Set X
⊢ ⇑(BumpCovering.single i s) = Pi.single i 1

Tactic:
rfl

Goal state after:
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
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}.Finite
s : Set ι := {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
this✝ : Fintype ↑{i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
this : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ ↑s.toFinset
h : t i x₀ ≠ 0
⊢ ({x | ¬t i x = 0} ∩ u').Nonempty

Tactic:
use x₀

Goal state after:
case h
𝕜 : 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
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}.Finite
s : Set ι := ⋯
this✝ : Fintype ↑{i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
this : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ ↑s.toFinset
h : t i x₀ ≠ 0
⊢ x₀ ∈ {x | ¬t i x = 0} ∩ u'
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
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
⊢ u ⊆ Set.univ

Tactic:
grind

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

Goal state before:
pp: case zero
𝕜 : 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⟯
⊢ ⇑(0 • s) = 0

Tactic:
rfl

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
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
⊢ f.toPOUFun i x = (f i) x * ∏ j ∈ t with WellOrderingRel j i, (1 - (f j) x)

Tactic:
refine congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => ?_)

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → (f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - (f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ {j ∈ t | WellOrderingRel j i}
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: case succ
𝕜 : 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⟯
k : ℕ
ih : ⇑(k • s) = k • ⇑s
⊢ ⇑((k + 1) • s) = ⇑(k • s) + ⇑s

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3.inr
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j ∈ v.carrier
⊢ closure (v.toFun j) ⊆ u j

Tactic:
exact v.closure_subset hj

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
i : ι
⊢ i ∈ v.carrier

Tactic:
by_contra! hi

Goal state after:
case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
i : ι
hi : i ∉ v.carrier
⊢ False
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
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
by
  obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl
    (subset_compl_iff_disjoint_left.mpr hd.symm)
  obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
    (subset_compl_comm.mp hut)
  obtain ⟨f, hfu, hfv, hf⟩ := exists_contMDiffMap_zero_one_of_isClosed I isClosed_closure
    isClosed_closure (subset_compl_iff_disjoint_left.mp hvu) (n := n)
  refine ⟨f, ?_, ?_, hf⟩
  · exact eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu
  · exact eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv

Goal state after:
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
⊢ ∃ ε, 0 < ε ∧ x ∉ thickening ε s

Tactic:
by
          rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs
          simpa using hxs

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
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I
L'_cont : Continuous ⇑L'
A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm
⊢ map (⇑(↑L' ∘ₗ P ∘ₗ ↑M.symm)) μ = map ((⇑L' ∘ ⇑P) ∘ ⇑M.symm) μ

Tactic:
rfl

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

Goal state before:
pp: case hd₀
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
j : ι✝
⊢ Tendsto (fun i_1 ↦ Pi.single i (d i_1) j) l (𝓝 (0 j))

Tactic:
rcases eq_or_ne j i with rfl | hj

Goal state after:
case hd₀.inl
𝕜 : 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
inst✝ : DecidableEq ι✝
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
j : ι✝
hi : ∀ (j_1 : ι✝), j_1 ≠ j → x j_1 ∈ closure[inst✝³ j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun i ↦ Pi.single j (d i) j) l (𝓝 (0 j))

case hd₀.inr
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
j : ι✝
hj : j ≠ i
⊢ Tendsto (fun i_1 ↦ Pi.single i (d i_1) j) l (𝓝 (0 j))
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: case hds
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι✝
⊢ (x + Pi.single i (d n)) j ∈ closure[inst✝³ j] (s j)

Tactic:
rcases eq_or_ne j i with rfl | hj

Goal state after:
case hds.inl
𝕜 : 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
inst✝ : DecidableEq ι✝
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
n : ι
j : ι✝
hi : ∀ (j_1 : ι✝), j_1 ≠ j → x j_1 ∈ closure[inst✝³ j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
hn : x j + d n ∈ s j
⊢ (x + Pi.single j (d n)) j ∈ closure[inst✝³ j] (s j)

case hds.inr
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
n : ι
hn : x i + d n ∈ s i
j : ι✝
hj : j ≠ i
⊢ (x + Pi.single i (d n)) j ∈ closure[inst✝³ j] (s j)
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case neg
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 ∉ support f
⊢ 0 < f x + g x

Tactic:
have : 0 < g x := by
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
      linarith [f_pos x]

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

Goal state before:
pp: case hcd
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
j : ι✝
⊢ Tendsto (fun i_1 ↦ (c i_1 • Pi.single i (d i_1)) j) l (𝓝 (Pi.single i y j))

Tactic:
rcases eq_or_ne j i with rfl | hj

Goal state after:
case hcd.inl
𝕜 : 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
inst✝ : DecidableEq ι✝
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
j : ι✝
hi : ∀ (j_1 : ι✝), j_1 ≠ j → x j_1 ∈ closure[inst✝³ j_1] (s j_1)
y : E j
hy : y ∈ tangentConeAt 𝕜 (s j) (x j)
d : ι → E j
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x j + d n ∈ s j
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun i ↦ (c i • Pi.single j (d i)) j) l (𝓝 (Pi.single j y j))

case hcd.inr
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
j : ι✝
hj : j ≠ i
⊢ Tendsto (fun i_1 ↦ (c i_1 • Pi.single i (d i_1)) j) l (𝓝 (Pi.single i y j))
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
x✝ : True
n : ℕ
hn : n ∈ Set.Ici N
⊢ (fun x ↦ c ^ x) n • d n ∈ Metric.ball 0 ((1 / 2) ^ N)

Tactic:
Set.mem_Ici

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
N : ℕ
x✝ : True
n : ℕ
hn : N ≤ n
⊢ (fun x ↦ c ^ x) n • d n ∈ Metric.ball 0 ((1 / 2) ^ N)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope

Goal state before:
pp: case inl.x
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 = c
⊢ a ∈ Icc a (b + c)

Tactic:
grind

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

Goal state before:
pp: case inl.x
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 = c
⊢ b ∈ Icc a (b + c)

Tactic:
grind

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

Goal state before:
pp: case inl.a
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 = c
⊢ a ≤ b

Tactic:
grind

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
this : 0 ≤ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2
⊢ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2

Tactic:
grind

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ ENNReal.ofReal (g b - g a) = ENNReal.ofReal (f b - f a)

Tactic:
grind

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

Goal state before:
pp: a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
i : ℕ
hi : i < n
hnI :
  (∀ i < n, (min a b ≤ (I i).1 ∧ (I i).1 ≤ max a b) ∧ min a b ≤ (I i).2 ∧ (I i).2 ≤ max a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
⊢ uIoc (I i).1 (I i).2 ⊆ uIoc a b

Tactic:
grind

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

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)

Tactic:
uIcc_of_le (by linarith)

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope

Goal state before:
pp: case inr
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
⊢ f (b + c) - f a ≤ f (b + c) - f a

Tactic:
rfl

Goal state after: