mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
⊢ SecondCountableTopology M

Tactic:
by
  obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
    countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x
  exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc

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

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 M
inst✝² : TopologicalSpace M'
inst✝¹ : TopologicalSpace H
inst✝ : ChartedSpace H M
f : M → M'
hf : IsLocalHomeomorph f
g : M' → M
hg : Function.RightInverse g f
q : M'
⊢ q ∈ (hf.localInverseAt (g q) ≫ₕ chartAt H (g q)).source

Tactic:
by
    nth_rw 3 [← hg.eq q]
    simp

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

Goal state before:
pp: case he
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
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
s : Opens M
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph (↥s) H
w✝¹ : Set (OpenPartialHomeomorph (↥s) H)
x : ↥s
he : e = (chartAt H ↑x).subtypeRestr ⋯
hc : (fun x ↦ {(chartAt H ↑x).subtypeRestr ⋯}) x = w✝¹
w✝ : Set (OpenPartialHomeomorph (↥s) H)
x' : ↥s
he' : e' = (chartAt H ↑x').subtypeRestr ⋯
hc' : (fun x ↦ {(chartAt H ↑x).subtypeRestr ⋯}) x' = w✝
⊢ (chartAt H ↑x).symm ≫ₕ chartAt H ↑x' ∈ G

Tactic:
exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)

Goal state after:
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, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G

Tactic:
let s := (c.symm ≫ₕ f₁).source ∩ c.symm ≫ₕ f₁ ⁻¹' g.source

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
⊢ ∃ s, IsOpen[inst✝⁶] s ∧ x ∈ s ∧ (c.symm ≫ₕ (e.trans e'.toHomeomorph).toOpenPartialHomeomorph ≫ₕ c').restr s ∈ G
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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑φ
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ↑φ.symm
this✝ : range ↑φ = φ.target
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ Convex ℝ univ

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E

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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑φ
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ↑φ.symm
this✝¹ : range ↑φ = φ.target
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex ℝ univ
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
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : Convex ℝ s
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ Convex ℝ s

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : IsRCLikeNormedField 𝕜
s : Set E
hs : Convex ℝ s
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex ℝ s
Module: Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ UniqueDiffOn 𝕜 (range ↑I)

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E

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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniqueDiffOn 𝕜 (range ↑I)
Module: Mathlib.Geometry.Manifold.IsManifold.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
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E

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
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ range ↑I ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range ↑I))
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this✝ : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')

Tactic:
let := NormedSpace.restrictScalars ℝ 𝕜 E

Goal state after:
case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type w
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
this✝¹ : (range fun x ↦ (↑I x.1, ↑I' x.2)) = range (Prod.map ↑I ↑I')
h : IsRCLikeNormedField 𝕜
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ Convex ℝ (range ↑I ×ˢ range ↑I')
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✝
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_6
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type u_7
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H : Type u_8
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I n M
M' : Type u_11
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : f1 ∈ atlas H M
f2 : OpenPartialHomeomorph M' H'
hf2 : f2 ∈ atlas H' M'
g1 : OpenPartialHomeomorph M H
hg1 : g1 ∈ atlas H M
g2 : OpenPartialHomeomorph M' H'
hg2 : g2 ∈ atlas H' M'
⊢ (f1.prod f2).symm ≫ₕ g1.prod g2 ∈ contDiffGroupoid n (I.prod I')

Tactic:
OpenPartialHomeomorph.prod_symm,

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✝
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_6
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type u_7
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H : Type u_8
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_9
inst✝⁶ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_10
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I n M
M' : Type u_11
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' n M'
f1 : OpenPartialHomeomorph M H
hf1 : f1 ∈ atlas H M
f2 : OpenPartialHomeomorph M' H'
hf2 : f2 ∈ atlas H' M'
g1 : OpenPartialHomeomorph M H
hg1 : g1 ∈ atlas H M
g2 : OpenPartialHomeomorph M' H'
hg2 : g2 ∈ atlas H' M'
⊢ f1.symm.prod f2.symm ≫ₕ g1.prod g2 ∈ contDiffGroupoid n (I.prod I')
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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
M' : Type u_16
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inl x)) (Sum.inl x))
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inl x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inl x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inl x)) (Sum.inl x))

Tactic:
apply this.congr_of_eventuallyEq

Goal state after:
case inl.h₁
𝕜 : 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 ℕ∞
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inl x)) (Sum.inl x))
⊢ ↑(extChartAt J (Sum.elim f g (Sum.inl x))) ∘
      Sum.elim f g ∘ ↑(extChartAt I (Sum.inl x)).symm =ᶠ[𝓝[range ↑I] ↑(extChartAt I (Sum.inl x)) (Sum.inl x)]
    ↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm

case inl.hx
𝕜 : 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 ℕ∞
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inl x)) (Sum.inl x))
⊢ (↑(extChartAt J (Sum.elim f g (Sum.inl x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inl x)).symm)
      (↑(extChartAt I (Sum.inl x)) (Sum.inl x)) =
    (↑(extChartAt J (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I (Sum.inl x)) (Sum.inl x))
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

Goal state before:
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
M' : Type u_16
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
    (range ↑I) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))

Tactic:
apply this.congr_of_eventuallyEq

Goal state after:
case inr.h₁
𝕜 : 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 ℕ∞
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ ↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘
      Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm =ᶠ[𝓝[range ↑I] ↑(extChartAt I (Sum.inr x)) (Sum.inr x)]
    ↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm

case inr.hx
𝕜 : 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 ℕ∞
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
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
g : M' → N
hf : ContMDiff I J n f
hg : ContMDiff I J n g
x : M'
this :
  ContDiffWithinAt 𝕜 n (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (range ↑I)
    (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
⊢ (↑(extChartAt J (Sum.elim f g (Sum.inr x))) ∘ Sum.elim f g ∘ ↑(extChartAt I (Sum.inr x)).symm)
      (↑(extChartAt I (Sum.inr x)) (Sum.inr x)) =
    (↑(extChartAt J (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I (Sum.inr x)) (Sum.inr x))
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'
x : M
n : ℕ∞ω
⊢ ContMDiffAt I I' n f x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
by
  rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_source]
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜
hx : x ≠ 0
⊢ ContMDiffAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) n (fun y ↦ y⁻¹) x

Tactic:
change ContMDiffAt 𝓘(𝕜) 𝓘(𝕜) n Inv.inv x
    rw [contMDiffAt_iff_contDiffAt]
    exact contDiffAt_inv 𝕜 hx

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
⊢ IsOpen[inst✝⁷] U

Tactic:
rw [hUu']

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
U : Set B
hU : e.source = U ×ˢ univ
φ : ↑U → B → F ≃L[𝕜] F
u : ↑U → Set B
hu : ∀ (x : ↑U), IsOpen[inst✝⁷] (u x)
hUu : ∀ (x : ↑U), u x ⊆ U
hux : ∀ (x : ↑U), ↑x ∈ u x
hφ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑U), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑U), (e.restr (u x ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
heuφ : ∀ (x : ↑U), EqOn (↑e) (fun q ↦ (q.1, (φ x q.1) q.2)) (u x ×ˢ univ)
huφ : ∀ (x x' : ↑U), ∀ y ∈ u x, y ∈ u x' → φ x y = φ x' y
hUu' : U = ⋃ i, u i
⊢ IsOpen[inst✝⁷] (⋃ i, u i)
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
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
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬↑(extChartAt I x) x = z

Tactic:
exact Ne.symm h'z

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 f₁ : M → M'
x : M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[univ] f x f'
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ f₁ =ᶠ[𝓝[univ] x] f

Tactic:
rwa [nhdsWithin_univ]

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

Tactic:
convert! hf.prodMap 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'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
x : M
f : M → M'
g : N → N'
y : N
hf : MDiffAt[univ] f x
hg : MDiffAt[univ] g y
⊢ univ = univ ×ˢ univ