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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
a✝ : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx with ⟨e, heG, hef, hex⟩

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
a✝ : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
⊢ ∃ e ∈ G, EqOn (↑e' ∘ f) (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx with ⟨e, heG, hef, hex⟩

Goal state after:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : OpenPartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn (↑e' ∘ f) (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source
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
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
⊢ ∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
have : HasGroupoid M (contDiffGroupoid n I) := hasGroupoid_of_pregroupoid _ (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
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h :
  ∀ (e e' : OpenPartialHomeomorph M H),
    e ∈ atlas H M →
      e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm ≫ₕ e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑I)
this : HasGroupoid M (contDiffGroupoid n I)
⊢ ∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid n I
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'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n f x

Tactic:
rw [Subsingleton.elim f fun _ => (f x)]

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
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
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : ℕ∞ω
inst✝ : Subsingleton M'
x : M
⊢ ContMDiffAt I I' n (fun x_1 ↦ f x) x
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst✝⁷] s
⊢ ContMDiffAt I I' n (s.piecewise f g) x

Tactic:
apply (hg x).congr_of_eventuallyEq

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
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
inst✝¹ : ChartedSpace H' M'
n : ℕ∞ω
f g : M → M'
s : Set M
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : ContMDiff I I' n f
hg : ContMDiff I I' n g
hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g
x : M
hx : x ∉ interior s
h'x : x ∉ closure[inst✝⁷] s
⊢ s.piecewise f g =ᶠ[𝓝 x] g
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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
M' : Type u_16
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
n : WithTop ℕ∞
x : M'
C : OpenPartialHomeomorph M' H := chartAt H x
hC : C = chartAt H x
this : ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I x) x
y : E
hy : y ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ (↑(extChartAt I (Sum.inr x)) ∘ Sum.inr ∘ ↑(extChartAt I x).symm) y = id y

Tactic:
simp [extChartAt, sum_chartAt_inr, ← hC, Sum.inr_injective.extend_apply C, C.right_inv hy.1,
    I.right_inv hy.2]

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
⊢ ContMDiffOn I I' 0 f s ↔ ContinuousOn f s

Tactic:
rw [contMDiffOn_iff]

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 : M → M'
s : Set M
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 0 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))) ↔
    ContinuousOn f s
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'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
exact extChartAt_preimage_mem_nhdsWithin h

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
⊢ ∀ (e e' : Trivialization (F₁ × F₂) TotalSpace.proj) [inst : MemTrivializationAtlas e]
    [inst_1 : MemTrivializationAtlas e'], ContinuousOn (fun b ↦ ↑(coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
by
    rintro _ _ ⟨e₁, e₂, he₁, he₂, rfl⟩ ⟨e₁', e₂', he₁', he₂', rfl⟩
    refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_ <;>
      dsimp only [prod_baseSet, mfld_simps]
    · mfld_set_tac
    · mfld_set_tac
    · rintro b hb
      rw [ContinuousLinearMap.ext_iff]
      rintro ⟨v₁, v₂⟩
      change (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
        (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
      rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
      exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]

Goal state after:
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
⊢ (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

Tactic:
rw [if_neg h, if_neg]

Goal state after:
case neg.hnc
𝕜 : 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
⊢ ¬MDiffAt[s] 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'
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' → M''
p : M × M'
hf : MDiffAt f p
⊢ mfderiv% f p = (mfderiv% fun z ↦ f (z.1, p.2)) p + (mfderiv% fun z ↦ f (p.1, z.2)) p

Tactic:
erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prodMk mdifferentiableAt_const) rfl,
    mfderiv_comp_of_eq hf (mdifferentiableAt_const.prodMk mdifferentiableAt_snd) rfl,
    ← ContinuousLinearMap.comp_add,
    mdifferentiableAt_fst.mfderiv_prod mdifferentiableAt_const,
    mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_snd, mfderiv_fst,
    mfderiv_snd, mfderiv_const, mfderiv_const]
  symm
  convert! ContinuousLinearMap.comp_id <| mfderiv% f (p.1, p.2)
  exact ContinuousLinearMap.coprod_inl_inr

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
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✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑e.symm) e.target

Tactic:
rw [e.contMDiffOn_iff e.toOpenPartialHomeomorph.mapsTo_symm]

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
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✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
⊢ ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB n (fun x ↦ (↑e.symm x).proj) e.target ∧
    ContMDiffOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) n (fun x ↦ (↑e (↑e.symm x)).2) e.target
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun

Tactic:
by
      let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩
      have : Continuous (chartAt (ModelProd H E) p).symm := by
        rw [← continuousOn_univ]
        convert! (chartAt (ModelProd H E) p).symm.continuousOn
        simp only [mfld_simps]
      simpa only [mfld_simps] using this

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

Goal state before:
pp: case e'_11
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = prodChartedSpace H H E E

pp: case hg.convert_11
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ChartedSpace H H

Tactic:
rw [chartedSpaceSelf_prod]

Goal state after:
case e'_11
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
e_10✝ : instTopologicalSpaceModelProd H E = instTopologicalSpaceProd
⊢ chartedSpaceSelf (ModelProd H E) = chartedSpaceSelf (H × E)
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
⊢ UniqueMDiffAt[f '' s] (f x)

Tactic:
by
  /- Rewrite in coordinates, apply `HasFDerivWithinAt.uniqueDiffWithinAt`. -/
  have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds (I := I') (f x))
  refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
  case pt => simp only [mfld_simps]
  case sub1 => mfld_set_tac
  case sub2 =>
    rintro _ ⟨y, ⟨⟨hys, hfy⟩, -⟩, rfl⟩
    exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩

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

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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (chartAt H c).source ∩ support (↑f.toContDiffBump ∘ ↑(extChartAt I c)) =
    (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut

Tactic:
support_comp_eq_preimage,

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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' support ↑f.toContDiffBump =
    (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : 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
⊢ ∃ v', v < v'

Tactic:
classical
  refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩
  · intro j
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
  · refine fun x hx => mem_iUnion.2 ?_
    by_cases! h : ∃ j ≠ i, x ∈ v j
    · rcases h with ⟨j, hji, hj⟩
      use j
      rwa [update_of_ne hji]
    · use i
      rw [update_self]
      exact hvi ⟨hx, mem_biInter h⟩
  · rintro j (rfl | hj)
    · rwa [update_self, ← v.apply_eq hi]
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj
  · exact fun _ => trivial
  · intro j hj
    rw [mem_insert_iff, not_or] at hj
    rw [update_of_ne hj.1, v.apply_eq hj.2]
  · refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
  · exact fun hle => hi (hle.1 <| mem_insert _ _)

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
⊢ FinStronglyMeasurable f μ

Tactic:
let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)

Goal state after:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ FinStronglyMeasurable f μ
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s

Tactic:
support_comp_eq_preimage,

Goal state after:
case refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ ↑I ⁻¹' support f = s
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ f =ᵐ[μ.restrict t] g

Tactic:
← sub_ae_eq_zero

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ f - g =ᵐ[μ.restrict t] 0