mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, rootMultiplicity x (derivative p) +
      (((derivative p).roots.toFinset \ p.roots.toFinset).card + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)

Tactic:
simp only [← count_roots, Finset.card_eq_sum_ones]

Goal state after:
p : ℝ[X]
⊢ ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, 1 + 1) ≤
    ∑ x ∈ p.roots.toFinset, Multiset.count x (derivative p).roots +
      (∑ x ∈ (derivative p).roots.toFinset \ p.roots.toFinset, Multiset.count x (derivative p).roots + 1)
Module: Mathlib.Analysis.Calculus.LocalExtr.Polynomial

Goal state before:
pp: p : ℝ[X]
⊢ ∀ x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset,
    x ∉ (derivative p).roots.toFinset → Multiset.count x (derivative p).roots = 0

Tactic:
intro x _ hx₂

Goal state after:
p : ℝ[X]
x : ℝ
a✝ : x ∈ p.roots.toFinset ∪ (derivative p).roots.toFinset
hx₂ : x ∉ (derivative p).roots.toFinset
⊢ Multiset.count x (derivative p).roots = 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
by_cases hE : CompleteSpace E

Goal state after:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

case neg
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : ¬CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
x : ℝ
⊢ x ∈ Ioi 0 → ∃ x_1 ∈ Ioi 0, x_1 ^ p = x

Tactic:
· exact fun hx ↦ ⟨x ^ (1 / p), rpow_pos_of_pos hx _, by simp [← rpow_mul (le_of_lt hx), hp]⟩

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z ↦ DifferentiableAt ℂ f z) x}
⊢ ContinuousOn f (closedBall c ↑R)

Tactic:
refine fun z hz => ContinuousAt.continuousWithinAt ?_

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
hc : ContinuousAt f c
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z ↦ DifferentiableAt ℂ f z) x}
z : ℂ
hz : z ∈ closedBall c ↑R
⊢ ContinuousAt f z
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∑' (n : ℕ), ↑(|(A n).det|.toNNReal + ε) * μ (s ∩ t n) = ∑' (n : ℕ), ↑ε * μ (s ∩ t n)

Tactic:
congr with n

Goal state after:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ ↑(|(A n).det|.toNNReal + ε) * μ (s ∩ t n) = ↑ε * μ (s ∩ t n)
Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : CommMonoid α
f : ι → β → α
g : β → α
s : Set β
inst✝ : UniformSpace α
⊢ HasProdUniformlyOn f g s ↔ TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, f i x2) g atTop s

Tactic:
by
  simpa [HasProdUniformlyOn, HasProd, ← UniformOnFun.ofFun_prod, Finset.prod_fn] using!
    UniformOnFun.tendsto_iff_tendstoUniformlyOn (𝔖 := {s})

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

Goal state before:
pp: case refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : LocallyPathConnectedSpace H
x : M
s : Set M
hs : s ∈ 𝓝 x
e : OpenPartialHomeomorph M H := ⋯
t : Set M := ⋯
ht : t ∈ 𝓝 x
⊢ pathComponentIn (↑e '' t) (↑e x) ∈ 𝓝 (↑e x)

Tactic:
exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
this :
  Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑0 * μ s))
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
this :
  Tendsto (fun ε ↦ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s) (𝓝[>] 0)
    (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
PG : Pregroupoid H
e e' : OpenPartialHomeomorph H H
he' : e ≈ e'
he : PG.property (↑e) e.source
⊢ PG.property (↑e') e.source

Tactic:
exact PG.congr e.open_source he'.eqOn.symm he

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

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
⊢ ∀ {e : OpenPartialHomeomorph H H}, e ∈ idRestrGroupoid → ∀ (s : Set H), IsOpen[inst✝] s → e.restr s ∈ idRestrGroupoid

Tactic:
rintro e ⟨s', hs', he⟩ s hs

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
s' : Set H
hs' : IsOpen[inst✝] s'
he : e ≈ ofSet s' hs'
s : Set H
hs : IsOpen[inst✝] s
⊢ e.restr s ∈ idRestrGroupoid
Module: Mathlib.Geometry.Manifold.IsManifold.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
x : H
⊢ map (↑I.symm) (𝓝[range ↑I] ↑I x) = 𝓝 x

Tactic:
by
  rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x) ↔ ContinuousWithinAt f s x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ContinuousWithinAt f s x

case refine_2
𝕜 : 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
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case inr.inl
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
hef : e = f.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
obtain (⟨f', hf', he'f'⟩ | ⟨f', hf', he'f'⟩) := ChartedSpace.mem_atlas_sum he'
      · rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]
        exact hM.compatible hf hf'
      · rw [hef, he'f']
        apply ContDiffGroupoid.mem_of_source_eq_empty
        ext x
        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩

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

Goal state before:
pp: case refine_2
𝕜 : 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
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'
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
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑e x))
hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)
A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source
⊢ ↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm =ᶠ[𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x]
    (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f

Tactic:
filter_upwards [A]
    rintro x' ⟨-, hfx'⟩
    simp only [*, e, e', (· ∘ ·), writtenInExtChartAt, e'.left_inv]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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'
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
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
n : ℕ∞ω
g : M' → M''
hg : ContMDiffOn I' I'' n g univ
hf : ContMDiffOn I I' n f univ
⊢ ContMDiffOn I I'' n (g ∘ f) univ

Tactic:
exact hg.comp hf subset_preimage_univ

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this : Tendsto (fun ε ↦ μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s) + 2 * ↑0 * μ s))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)

Tactic:
simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
h's : μ s ≠ ∞
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this : Tendsto (fun ε ↦ μ (f '' s) + 2 * ↑ε * μ s) (𝓝[>] 0) (𝓝 (μ (f '' s)))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he' : e' ∈ maximalAtlas I' n M'
hx : f x ∈ e'.source
h : ContinuousWithinAt f s x
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' n) (↑e' ∘ f) s x ↔
    LiftPropWithinAt (ContDiffWithinAtProp I 𝓘(𝕜, E') n) (↑(e'.extend I') ∘ f) s x

Tactic:
have A : ContinuousWithinAt ((e'.extend I') ∘ f) s x :=
    (e'.continuousAt_extend hx).comp_continuousWithinAt h

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' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
x : M
n : ℕ∞ω
he' : e' ∈ maximalAtlas I' n M'
hx : f x ∈ e'.source
h : ContinuousWithinAt f s x
A : ContinuousWithinAt (↑(e'.extend I') ∘ f) s x
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' n) (↑e' ∘ f) s x ↔
    LiftPropWithinAt (ContDiffWithinAtProp I 𝓘(𝕜, E') n) (↑(e'.extend I') ∘ f) s x
Module: Mathlib.Geometry.Manifold.MFDeriv.Defs

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ ∀ {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H},
    e ∈ contDiffGroupoid 1 I →
      x ∈ e.source →
        DifferentiableWithinAtProp I I' f s x → DifferentiableWithinAtProp I I' (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
by
      intro s x f e he hx h
      rw [DifferentiableWithinAtProp] at h ⊢
      have : I x = (I ∘ e.symm ∘ I.symm) (I (e x)) := by simp only [hx, mfld_simps]
      rw [this] at h
      have : I (e x) ∈ I.symm ⁻¹' e.target ∩ Set.range I := by simp only [hx, mfld_simps]
      have := (mem_groupoid_of_pregroupoid.2 he).2.contDiffWithinAt this
      convert! (h.comp' _ (this.differentiableWithinAt one_ne_zero)).mono_of_mem_nhdsWithin _
        using 1
      · ext y; simp only [mfld_simps]
      refine
        mem_nhdsWithin.mpr
          ⟨I.symm ⁻¹' e.target, e.open_target.preimage I.continuous_symm, by
            simp_rw [Set.mem_preimage, I.left_inv, e.mapsTo hx], ?_⟩
      mfld_set_tac

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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 : M → M'
s : Set M
x : M
n : ℕ∞
⊢ ContMDiffWithinAt I I' (↑n) f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x

Tactic:
by
  refine ⟨fun h m hm => h.of_le (mod_cast hm), fun h => ?_⟩
  obtain - | n := n
  · exact contMDiffWithinAt_infty.2 fun n => h n le_top
  · exact h n le_rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀
⊢ ContMDiffAt I' I n (fun x ↦ ∏ i ∈ t, f i x) x₀

Tactic:
simp only [← contMDiffWithinAt_univ] at *

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
x₀ : M
t : Finset ι
f : ι → M → G
h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) Set.univ x₀
⊢ ContMDiffWithinAt I' I n (fun x ↦ ∏ i ∈ t, f i x) Set.univ x₀
Module: Mathlib.Geometry.Manifold.MFDeriv.FDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)
⊢ HasMFDerivAt% f x f' ↔ HasFDerivAt f f' x

Tactic:
rw [← hasMFDerivWithinAt_univ, hasMFDerivWithinAt_iff_hasFDerivWithinAt, hasFDerivWithinAt_univ]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
n : ℕ∞ω
x : M
⊢ ContMDiffAt I 𝓘(𝕜, E) n (↑(extChartAt I x)) x

Tactic:
rw [contMDiffAt_iff_source]
  apply contMDiffWithinAt_id.congr_of_eventuallyEq_of_mem _ (by simp)
  filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
  exact PartialEquiv.right_inv (extChartAt I x) hy

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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ MDiff[s] f ↔ ContinuousOn f s ∧ ∀ (y : M'), MDiff[s ∩ f ⁻¹' (extChartAt I' y).source] (↑(extChartAt I' y) ∘ f)

Tactic:
simp only [mdifferentiableOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
    OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_trans, extChartAt,
    OpenPartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, and_congr_right_iff]
  intro h
  constructor
  · refine fun h' y => ⟨?_, fun x _ => h' x y⟩
    have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
    convert! (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h
    simp
  · exact fun h' x y => (h' y).2 x 0

Goal state after:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
e✝ : Pretrivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
v : F
⊢ (↑e { proj := b, snd := e.symm b v }).2 = v

Tactic:
e.apply_mk_symm hb v

Goal state after:
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: case pos
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸]
    (↑(if hb : b ∈ e.baseSet ∩ e'.baseSet then (linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯
        else LinearEquiv.refl R F)).toFun

Tactic:
rw [dif_pos hb]

Goal state after:
case pos
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F TotalSpace.proj
x : TotalSpace F E
b✝ : B
y : E b✝
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ Continuous[inst✝⁸, inst✝⁸] (↑((linearEquivAt R e b ⋯).symm ≪≫ₗ linearEquivAt R e' b ⋯)).toFun