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

Goal state before:
pp: a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] b) l

Tactic:
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)

Goal state after:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[<] b) l
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: case inl.inl
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : s ∩ Ioi a = ∅
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp [sdiff_eq, ← Iio_union_Ioi, inter_union_distrib_left, hs_Iio, hs_Ioi]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ ⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
by
  have := hφ.lintegral_tendsto_of_countably_generated hfm
  refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt
    (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => ?_
  exact (this.eventually_const_lt hw).exists

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

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) = volume (f '' s)

Tactic:
simpa using (lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn hs hf' hf 1).symm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ (Ioi a).indicator (fun x ↦ g (b * x)) x = (HMul.hMul b ⁻¹' Ioi (b * a)).indicator (g ∘ HMul.hMul b) x

Tactic:
preimage_const_mul_Ioi₀ _ hb,

Goal state after:
case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ (Ioi a).indicator (fun x ↦ g (b * x)) x = (Ioi (b * a / b)).indicator (g ∘ HMul.hMul b) x
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 : ℕ), μ (closedBall 0 R ∩ t n) = ↑ε * μ (⋃ n, closedBall 0 R ∩ t n)

Tactic:
rw [measure_iUnion]
      · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
      · intro n
        exact measurableSet_closedBall.inter (t_meas n)

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

Goal state before:
pp: case refine_3
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 := chartAt H x
t : Set M := s ∩ e.source
ht : t ∈ 𝓝 x
⊢ id (↑e.symm '' pathComponentIn (↑e '' t) (↑e x)) ⊆ t

Tactic:
exact (image_mono pathComponentIn_subset).trans
      (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
⊢ T1Space M

Tactic:
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
  by_cases hy : y ∈ (chartAt H x).source
  · refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
    · exact OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton
    · simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
        mem_singleton_iff, true_and]
      exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
  · exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩

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

Goal state before:
pp: H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : OpenPartialHomeomorph M H
⊢ e'' ∈ atlas H M → e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G

Tactic:
he''

Goal state after:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e e' : OpenPartialHomeomorph M H
h : e' ≈ e
he : e ∈ maximalAtlas M G
e'' : OpenPartialHomeomorph M H
he'' : e'' ∈ atlas H M
⊢ e'.symm ≫ₕ e'' ∈ G ∧ e''.symm ≫ₕ e' ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
⊢ e'' ∈ atlas H α → e'.symm ≫ₕ e'' ∈ G

Tactic:
he''

Goal state after:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e'.symm ≫ₕ e'' ∈ G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
have : x ∈ s := by
        constructor
        · simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toOpenPartialHomeomorph_source]
          rw [trans_source] at hx
          exact hx.1
        · exact hg₂

Goal state after:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace M'
inst✝² : TopologicalSpace M''
G : StructureGroupoid H
inst✝¹ : ChartedSpace H M'
inst✝ : ChartedSpace H M''
e : Structomorph G M M'
e' : Structomorph G M' M''
c : OpenPartialHomeomorph M H
c' : OpenPartialHomeomorph M'' H
hc : c ∈ atlas H M
hc' : c' ∈ atlas H M''
x : H
hx : x ∈ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').source
f₁ : OpenPartialHomeomorph M M' := e.toOpenPartialHomeomorph
f₂ : OpenPartialHomeomorph M' M'' := e'.toOpenPartialHomeomorph
f : OpenPartialHomeomorph M M'' := (e.trans e'.toHomeomorph).toOpenPartialHomeomorph
feq : f = f₁ ≫ₕ f₂
y : M' := ↑(c.symm ≫ₕ f₁) x
g : OpenPartialHomeomorph M' H := chartAt H y
hg₁ : chartAt H y ∈ atlas H M'
hg₂ : y ∈ (chartAt H y).source
s : Set H := (c.symm ≫ₕ f₁).source ∩ ↑(c.symm ≫ₕ f₁) ⁻¹' g.source
open_s : IsOpen[inst✝⁶] s
this : x ∈ s
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
⊢ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ hes

Goal state after:
case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : OpenPartialHomeomorph H H
s : Set H
hs : IsOpen[inst✝] s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G
Module: Mathlib.Geometry.Manifold.IsManifold.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
inst✝ : NormedSpace ℝ E
h : ¬IsRCLikeNormedField 𝕜
⊢ Convex ℝ (range ↑I)

Tactic:
simp [range_eq_univ_of_not_isRCLikeNormedField I h, convex_univ]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ (extChartAt I x).target ⊆ range ↑I

Tactic:
by
  simp only [mfld_simps]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Tactic:
by
  simp only [mfld_simps]

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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
n : ℕ∞ω
he : e ∈ maximalAtlas I n M
hs : s ⊆ e.source
⊢ ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)

Tactic:
by
  simp_rw [ContMDiffOn, Set.forall_mem_image]
  refine forall₂_congr fun x hx => ?_
  rw [contMDiffWithinAt_iff_source_of_mem_maximalAtlas he (hs hx)]
  apply contMDiffWithinAt_congr_set
  simp_rw [e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]

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 : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
by
  -- WLOG, `x ∈ s`, otherwise we add `x` to `s`
  wlog hxs : x ∈ s generalizing s
  · rw [← contMDiffWithinAt_insert_self, this (mem_insert _ _), insert_idem]
  rw [insert_eq_of_mem hxs]
  -- The `←` implication is trivial
  refine ⟨fun h ↦ ?_, fun ⟨u, hmem, hu⟩ ↦
    (hu _ (mem_of_mem_nhdsWithin hxs hmem)).mono_of_mem_nhdsWithin hmem⟩
  -- The property is true in charts. Let `v` be a good neighborhood in the chart where the function
  -- is `Cⁿ`.
  rcases (contMDiffWithinAt_iff'.1 h).2.contDiffOn le_rfl (by simp [hn]) with ⟨v, hmem, hsub, hv⟩
  have hxs' : extChartAt I x x ∈ (extChartAt I x).target ∩
      (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) :=
    ⟨(extChartAt I x).map_source (mem_extChartAt_source _), by rwa [extChartAt_to_inv], by
      rw [extChartAt_to_inv]; apply mem_extChartAt_source⟩
  rw [insert_eq_of_mem hxs'] at hmem hsub
  -- Then `(extChartAt I x).symm '' v` is the neighborhood we are looking for.
  refine ⟨(extChartAt I x).symm '' v, ?_, ?_⟩
  · rw [← map_extChartAt_symm_nhdsWithin (I := I),
      h.1.nhdsWithin_extChartAt_symm_preimage_inter_range (I := I) (I' := I')]
    exact image_mem_map hmem
  · have hv₁ : (extChartAt I x).symm '' v ⊆ (extChartAt I x).source :=
      image_subset_iff.2 fun y hy ↦ (extChartAt I x).map_target (hsub hy).1
    have hv₂ : MapsTo f ((extChartAt I x).symm '' v) (extChartAt I' (f x)).source := by
      rintro _ ⟨y, hy, rfl⟩
      exact (hsub hy).2.2
    rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, PartialEquiv.image_symm_image_of_subset_target]
    exact hsub.trans inter_subset_left

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

Goal state before:
pp: case neg
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∉ e.baseSet
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝² b] (Trivialization.symmₗ R e b).toFun

Tactic:
exact continuous_zero.congr fun x => (e.symmₗ_apply_of_notMem hb x).symm

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'
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), MDiff[s i] f
hs : ∀ (i : ι), IsOpen[inst✝⁶] (s i)
x : M
i : ι
hxsi : x ∈ (fun i ↦ s i) i
⊢ MDiffAt[⋃ i, s i] f x

Tactic:
exact (hf i).mdifferentiableAt ((hs i).mem_nhds hxsi) |>.mdifferentiableWithinAt

Goal state after:
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
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
hz : z ∈ ↑(extChartAt I x).symm ⁻¹' u ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ)
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
⊢ z ∈ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ↔ z ∈ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_union, mem_compl_iff, hIz, not_true_eq_false,
      or_false, and_true] at hz ⊢

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
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
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm z ∈ s ↔ ↑(extChartAt I x).symm z ∈ t
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
⊢ Trivialization.continuousLinearMapAt R (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b

Tactic:
ext1 v
  simp_all
  rfl

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

Goal state before:
pp: case refine_1.ex
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ (f x).proj ∈ (trivializationAt F E (f x₀).proj).baseSet

Tactic:
exact hx

Goal state after:
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
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDiff f ↔ MDiff (Prod.fst ∘ f) ∧ MDiff (Prod.snd ∘ f)

Tactic:
by
  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
  exact mdifferentiable_prod_iff f

Goal state after:
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
z : E
h : z ∈ (extChartAt I x).target
⊢ MDiffAt[range ↑I] ↑(extChartAt I x).symm z

Tactic:
have Z := I.mdifferentiableWithinAt_symm (extChartAt_target_subset_range x 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
inst✝ : IsManifold I 1 M
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDiffAt[range ↑I] ↑I.symm z
⊢ MDiffAt[range ↑I] ↑(extChartAt I x).symm z
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed[inst✝¹] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst✝¹] (u i)
us : s ⊆ ⋃ i, u i
⊢ univ ⊆ ⋃ i, Option.elim' sᶜ u i

Tactic:
simp_rw [← compl_union_self s, Option.elim', iUnion_option]

Goal state after:
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed[inst✝¹] s
u : ι → Set X
uo : ∀ (i : ι), IsOpen[inst✝¹] (u i)
us : s ⊆ ⋃ i, u i
⊢ sᶜ ∪ s ⊆ sᶜ ∪ ⋃ a, u a
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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
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
i : ι
s : Finset ι
hi : i ∉ s
h :
  (∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀) →
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs : ∀ i_1 ∈ insert i s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i_1 x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x + ∑ i ∈ s, t i x⟩) u x₀

Tactic:
apply (hs _ (s.mem_insert_self i)).add_section

Goal state after:
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
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
i : ι
s : Finset ι
hi : i ∉ s
h :
  (∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀) →
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs : ∀ i_1 ∈ insert i s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i_1 x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀