mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IsManifold.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
s : Set H
⊢ ↑I.symm ⁻¹' s ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I

Tactic:
I.toPartialEquiv_coe_symm

Goal state after:
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
s : Set H
⊢ ↑I.symm ⁻¹' s ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
pp: 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
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
y : E × F
hy :
  y ∈
    (extChartAt (I.prod J) p).target ∩ ↑(extChartAt (I.prod J) p).symm ⁻¹' (s ∩ Prod.snd ⁻¹' (extChartAt J p.2).source)
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) y = y.2

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
inst✝⁵ : ChartedSpace H M
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) =
    (↑(extChartAt (I.prod J) p) p).2

Tactic:
· exact (extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩

Goal state after:
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
inst✝⁵ : ChartedSpace H M
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
s : Set (M × N)
p : M × N
⊢ (↑(extChartAt J p.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod J) p).symm) (↑(extChartAt (I.prod J) p) p) =
    (↑(extChartAt (I.prod J) p) p).2
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'
n : ℕ∞ω
c : M'
x : M
⊢ ContinuousWithinAt (fun x ↦ c) univ x

Tactic:
fun_prop

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
n : ℕ∞ω
x : H
⊢ ContDiffWithinAtProp I I n id univ x

Tactic:
by
  simp only [ContDiffWithinAtProp, id_comp, preimage_univ, univ_inter]
  have : ContDiffWithinAt 𝕜 n id (range I) (I x) := contDiff_id.contDiffAt.contDiffWithinAt
  refine this.congr (fun y hy => ?_) ?_
  · simp only [ModelWithCorners.right_inv I hy, mfld_simps]
  · simp only [mfld_simps]

Goal state after:
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
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x ↦ default
this : aux ∘ Sum.inl ∘ f = f
⊢ ContMDiffOn I J n (aux ∘ Sum.inl ∘ f) univ

Tactic:
apply (contMDiff_id.sumElim contMDiff_const).contMDiffOn (s := @Sum.inl N N' '' univ).comp 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
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := ⋯
this : aux ∘ Sum.inl ∘ f = f
⊢ univ ⊆ Sum.inl ∘ f ⁻¹' Sum.inl '' univ
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'
U : TopologicalSpace.Opens M'
f : M → ↥U
x : M
⊢ ContMDiffAt I I' ∞ (Subtype.val ∘ f) x ↔ ContMDiffAt I I' ∞ f x

Tactic:
rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]

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

Goal state before:
pp: case right
𝕜 : 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 : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' e ⁻¹' (extChartAt I y).source
⊢ ↑I (↑I.symm z) = z

Tactic:
rw [I.right_inv]
    apply mem_of_subset_of_mem _ hz.1
    exact letI := h.singletonChartedSpace; extChartAt_target_subset_range (I := I) x

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 t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x

Tactic:
← contMDiffWithinAt_insert_self (s := s),

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 t : Set M
x : M
n : ℕ∞ω
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f t x
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
n : ℕ∞ω
x : E
hx : x ∈ range ↑I
⊢ ContinuousWithinAt (↑I.symm) (range ↑I) x

Tactic:
fun_prop

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

Goal state before:
pp: case hs
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(c.symm ≫ₕ f ≫ₕ c')) (↑(chartAt H x).symm ⁻¹' f.source)
    (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
h1 : c' = chartAt H (↑f x)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ (c.symm ≫ₕ f ≫ₕ c').source ⊆ ↑(chartAt H x).symm ⁻¹' f.source

Tactic:
dsimp [x, c]; mfld_set_tac

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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x✝ : M := ↑f.symm X
hx✝ : x✝ ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x✝
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x✝)) ∘ ↑f ∘ ↑(chartAt H x✝).symm)
    (↑(chartAt H x✝).symm ⁻¹' f.source) (↑(chartAt H x✝) x✝)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x✝ ∈ e.source
h2X : ↑c' X = ↑e (↑c (↑f.symm X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm) (↑e.symm) (e.target ∩ e.target)
x : H
hx : x ∈ e.target
⊢ (↑c' ∘ ↑f ∘ ↑c.symm) (↑e.symm x) ∈ (c.symm ≫ₕ f ≫ₕ c').target

Tactic:
exact OpenPartialHomeomorph.mapsTo _ (h2e <| e.symm.mapsTo hx)

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

Goal state before:
pp: B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃

Tactic:
fun_prop

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

Goal state before:
pp: B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ ((p.1, p.2.1), p.1, p.2.2)

Tactic:
fun_prop

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

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
x : TotalSpace F (⇑f *ᵖ E)
h : f x.proj ∈ e.baseSet
⊢ TotalSpace.mk' F x.proj (e.symm (f x.proj) (↑e { proj := f x.proj, snd := x.snd }).2) = x

Tactic:
e.symm_apply_apply_mk h

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'
x : M
s : Set M
y : M
⊢ MDiffAt[insert y s] f x ↔ MDiffAt[s] f x

Tactic:
by
  rcases eq_or_ne x y with (rfl | h)
  · exact mdifferentiableWithinAt_insert_self
  have : T1Space M := I.t1Space M
  apply mdifferentiableWithinAt_congr_nhds
  exact nhdsWithin_insert_of_ne h

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

Goal state before:
pp: case 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
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 t : Set M
hf : MDiff[s] f
hf' : MDiff[t] f
hs : IsOpen[inst✝⁶] s
ht : IsOpen[inst✝⁶] t
x : M
hx : x ∈ s
⊢ MDiffAt[s ∪ t] f x

pp: case inr
𝕜 : 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 t : Set M
hf : MDiff[s] f
hf' : MDiff[t] f
hs : IsOpen[inst✝⁶] s
ht : IsOpen[inst✝⁶] t
x : M
hx : x ∈ t
⊢ MDiffAt[s ∪ t] f x

Tactic:
· exact (hf x hx).mdifferentiableAt (hs.mem_nhds hx) |>.mdifferentiableWithinAt

Goal state after:
case inr
𝕜 : 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 t : Set M
hf : MDiff[s] f
hf' : MDiff[t] f
hs : IsOpen[inst✝⁶] s
ht : IsOpen[inst✝⁶] t
x : M
hx : x ∈ t
⊢ MDiffAt[s ∪ t] f x
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✝⁹ : 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
x : B
hx : x ∈ e.baseSet
⊢ ↑e (zeroSection F E x) = (x, 0)

Tactic:
simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]

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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
h : MDiffAt[univ] f p.proj
⊢ tangentMapWithin I I' f s p = tangentMap I I' f p

Tactic:
rw [← tangentMapWithin_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 : M → M'
s : Set M
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
h : MDiffAt[univ] f p.proj
⊢ tangentMapWithin I I' f s p = tangentMapWithin I I' f univ p
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'
c : M'
x : M
⊢ ContinuousAt (fun x ↦ c) x

Tactic:
fun_prop

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''
u : Set M'
hg : MDiffAt[u] g (f x)
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f'
    (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
F : HasMFDerivAt[s] f x f'
⊢ MDiffAt[s] (g ∘ f) x

Tactic:
rcases hg.2 with ⟨g', hg'⟩

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''
u : Set M'
hg : MDiffAt[u] g (f x)
hf : MDiffAt[s] f x
h : s ⊆ f ⁻¹' u
f' : E →L[𝕜] E'
hf' :
  HasFDerivWithinAt (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) f'
    (↑I.symm ⁻¹' ↑(chartAt H x).symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
F : HasMFDerivAt[s] f x f'
g' : E' →L[𝕜] E''
hg' :
  HasFDerivWithinAt (↑I'' ∘ (↑(chartAt H'' (g (f x))) ∘ g ∘ ↑(chartAt H' (f x)).symm) ∘ ↑I'.symm) g'
    (↑I'.symm ⁻¹' ↑(chartAt H' (f x)).symm ⁻¹' u ∩ range ↑I') (↑I' (↑(chartAt H' (f x)) (f x)))
⊢ MDiffAt[s] (g ∘ 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% f (p.1, p.2) ∘SL (mfderiv% fun x ↦ (x.1, p.2)) p + (mfderiv% fun z ↦ f (p.1, z.2)) p

Tactic:
mfderiv_comp_of_eq hf (mdifferentiableAt_const.prodMk mdifferentiableAt_snd) rfl,

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' → M''
p : M × M'
hf : MDiffAt f p
⊢ mfderiv% f p =
    mfderiv% f (p.1, p.2) ∘SL (mfderiv% fun x ↦ (x.1, p.2)) p +
      mfderiv% f (p.1, p.2) ∘SL (mfderiv% fun x ↦ (p.1, x.2)) p
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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
⊢ ContinuousAt Sum.swap p

Tactic:
fun_prop

Goal state after: