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

Goal state before:
pp: case pos
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ mfderiv[s] f₁ x = mfderiv[s] f x

Tactic:
unfold mfderivWithin

Goal state after:
case pos
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDiffAt[s] f x
⊢ (if MDiffAt[s] f₁ x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f₁) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
    else 0) =
    if MDiffAt[s] f x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
    else 0
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

Goal state before:
pp: case neg
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ¬MDiffAt[s] f x
⊢ mfderiv[s] f₁ x = mfderiv[s] f x

Tactic:
unfold mfderivWithin

Goal state after:
case neg
𝕜 : 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'
f f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ¬MDiffAt[s] f x
⊢ (if MDiffAt[s] f₁ x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f₁) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
    else 0) =
    if MDiffAt[s] f x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
    else 0
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x

Tactic:
← mdifferentiableWithinAt_univ

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
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'
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M' × N'
⊢ MDiffAt[univ] f x ↔ MDiffAt[univ] (Prod.fst ∘ f) x ∧ MDiffAt[univ] (Prod.snd ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt f x
hg : MDiffAt g y
⊢ MDiffAt (Prod.map f g) (x, y)

Tactic:
← mdifferentiableWithinAt_univ

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
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'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ MDiffAt[univ] (Prod.map f g) (x, y)
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 : B
a✝ : y ∈ u
⊢ (↑(trivializationAt F E x) { proj := y, snd := s y }).2 = ?m.113

Tactic:
apply Subsingleton.elim

Goal state after:
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''
hg : MDiffAt g (f x)
hf : MDiffAt[s] f x
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
← mdifferentiableWithinAt_univ

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
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''
hg : MDiffAt[univ] g (f x)
hf : MDiffAt[s] f x
⊢ MDiffAt[s] (g ∘ f) x
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm y =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
have U : UniqueMDiffAt[range I] y := by
    apply I.uniqueMDiffOn
    exact extChartAt_target_subset_range x hy
  have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
  have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
    rwa [← extChartAt_source (I := I)]
  rw [← mfderiv_comp_mfderivWithin]; rotate_left
  · apply mdifferentiableAt_extChartAt h''y
  · exact mdifferentiableWithinAt_extChartAt_symm hy
  · exact U
  rw [← mfderivWithin_id U]
  apply Filter.EventuallyEq.mfderivWithin_eq
  · filter_upwards [extChartAt_target_mem_nhdsWithin_of_mem hy] with z hz
    simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hz, id_eq]
  · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: case hL
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffAt[(extChartAt I x).source] (↑(extChartAt I x).symm y)
this :
  mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    mfderiv[(extChartAt I x).source] ↑(extChartAt I x) (↑(extChartAt I x).symm y)
⊢ ↑(extChartAt I x).symm ∘ ↑(extChartAt I x) =ᶠ[𝓝[(extChartAt I x).source] ↑(extChartAt I x).symm y] id

Tactic:
filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffAt[(extChartAt I x).source] (↑(extChartAt I x).symm y)
this :
  mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    mfderiv[(extChartAt I x).source] ↑(extChartAt I x) (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) z = id z
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case insert
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
⊢ HasMFDerivAt[s] (f i * ∏ x ∈ t, f x) z (∑ x ∈ t, (∏ j ∈ (insert i t).erase x, f j z) • f' x + (∏ j ∈ t, f j z) • f' i)

Tactic:
convert! hf.1.mul (IH hf.2) using 2

Goal state after:
case e'_5
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
e_1✝ : (TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, F') ((f i * ∏ x ∈ t, f x) z)) = (TangentSpace I z →L[𝕜] F')
⊢ ∑ x ∈ t, (∏ j ∈ (insert i t).erase x, f j z) • f' x = f i z • ∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i

case e'_6
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t✝ : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  (∀ i ∈ t, HasMFDerivAt[s] (f i) z (f' i)) →
    HasMFDerivAt[s] (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)
hf : HasMFDerivAt[s] (f i) z (f' i) ∧ ∀ x ∈ t, HasMFDerivAt[s] (f x) z (f' x)
e_2✝ : (TangentSpace I z →L[𝕜] TangentSpace 𝓘(𝕜, F') ((f i * ∏ x ∈ t, f x) z)) = (TangentSpace I z →L[𝕜] F')
⊢ (∏ j ∈ t, f j z) • f' i = (∏ i ∈ t, f i) z • f' i
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∃ v, (∀ (a : ι), IsOpen[inst✝¹] (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a

Tactic:
refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (a : ι), IsOpen[inst✝¹] ((fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) a)

case refine_2
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ⋃ i, (fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) i = univ

case refine_3
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ LocallyFinite fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a

case refine_4
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (a : ι), (fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) a ⊆ u a
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst✝²] (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ a, e ⁻¹' U a = univ
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a

Tactic:
have heU : range e ⊆ ⋃ i, U i := by
      simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using! hu

Goal state after:
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst✝²] (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ a, e ⁻¹' U a = univ
heU : range e ⊆ ⋃ i, U i
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case inr
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ i, ∃ (_ : i ∈ c), x_1 ∈ i.carrier
this : Nonempty (PartialRefinement u s p)
⊢ ∃ i, x ∈ (find c ne i).toFun i

Tactic:
choose! v hvc hiv using hx

Goal state after:
case inr
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : ι → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
⊢ ∃ i, x ∈ (find c ne i).toFun i
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
⊢ 0 = ∫ (x : M) in s, f x ∂μ

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := hs.exists_isCompact_cthickening

Goal state after:
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)
⊢ 0 = ∫ (x : M) in s, f x ∂μ
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.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_2
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 𝓘(ℝ, ℝ) (↑n) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x / (f x + g x) ≤ 1

Tactic:
apply div_le_one_of_le₀ _ (A x).le

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
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 𝓘(ℝ, ℝ) (↑n) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x ≤ f x + g x