mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝¹ : CompleteSpace E
inst✝ : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ DifferentiableWithinAt ℂ f U x

Tactic:
have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2

Goal state after:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst✝¹ : CompleteSpace E
inst✝ : φ.NeBot
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
⊢ DifferentiableWithinAt ℂ f U x
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case pos.refine_1
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
x y : M
hxy : x ≠ y
hy : y ∈ (chartAt H x).source
⊢ IsOpen[inst✝²] ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) y}ᶜ)

Tactic:
exact OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton

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

Goal state before:
pp: case mpr
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
⊢ P f (s ∩ f ⁻¹' e'.source) x → P (↑e' ∘ f) (s ∩ f ⁻¹' e'.source) x

Tactic:
exact hG.left_invariance' he' inter_subset_right hxe'

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

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ ContinuousWithinAt f univ x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ) (↑(chartAt H x) x) ↔
    ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
continuousWithinAt_univ,

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ ContinuousAt f x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ) (↑(chartAt H x) x) ↔
    ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
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✝
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
H : Type u_5
inst✝ : TopologicalSpace H
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : Convex ℝ φ.target
hcont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑φ
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ↑φ.symm
hint : (interior φ.target).Nonempty
⊢ (interior (range ↑φ)).Nonempty

Tactic:
by
    have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
    simp [this, hint]

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
z : H
hz : z ∈ (e.symm ≫ₕ e').source
⊢ ↑I '' (e.symm ≫ₕ e').source ∈ 𝓝[range ↑I] ↑I z

Tactic:
exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)

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

Goal state before:
pp: case refine_1
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ fderivWithin 𝕜 (↑φ) φ.source (↑φ.symm (↑φ x)) ∘SL fderivWithin 𝕜 (↑φ.symm) φ.target (↑φ (↑φ.symm (↑φ x))) =
    ContinuousLinearMap.id 𝕜 E

Tactic:
φ.right_inv (φ.map_source hx),

Goal state after:
case refine_1
𝕜 : 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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
hn : n ≠ 0
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
φ : PartialEquiv E E := extendCoordChange e e'
hx : x ∈ φ.source
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφ' : ContDiffOn 𝕜 n (↑φ.symm) φ.target
⊢ fderivWithin 𝕜 (↑φ) φ.source (↑φ.symm (↑φ x)) ∘SL fderivWithin 𝕜 (↑φ.symm) φ.target (↑φ x) =
    ContinuousLinearMap.id 𝕜 E
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ ContinuousWithinAt f univ ↑x ↔ ContinuousWithinAt (f ∘ Subtype.val) univ x

Tactic:
continuousWithinAt_univ,

Goal state after:
case refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U : Opens M
f : M → M'
x : ↥U
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ Subtype.val) x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ ContinuousWithinAt f univ (inclusion hUV x) ↔ ContinuousWithinAt (f ∘ inclusion hUV) univ x

Tactic:
continuousWithinAt_univ,

Goal state after:
case refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
U V : Opens M
hUV : U ≤ V
f : ↥V → M'
x : ↥U
⊢ ContinuousAt f (inclusion hUV x) ↔ ContinuousAt (f ∘ inclusion hUV) x
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},
    e' ∈ G →
      s ⊆ f ⁻¹' e'.source →
        f x ∈ e'.source → G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt (↑e' ∘ f) s x

Tactic:
intro s x f e' he'G _ hfx h hx
      rcases h hx with ⟨e, heG, hef, hex⟩
      refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩
      · intro y hy
        simp only [mfld_simps] at hy
        simp only [hef ⟨hy.1, hy.2.1⟩, mfld_simps]
      · simpa only [hex, hef ⟨hx, hex⟩, mfld_simps] using hfx

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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
⊢ ContMDiffAt I I' n (s.piecewise f g) x

Tactic:
apply (hf x).congr_of_eventuallyEq

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
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
⊢ s.piecewise f g =ᶠ[𝓝 x] f
Module: Mathlib.Geometry.Manifold.ContMDiff.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
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
this : x ∈ frontier s
⊢ ContMDiffAt I I' n (s.piecewise f g) x

Tactic:
apply (hf x).congr_of_eventuallyEq

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
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
this : x ∈ frontier s
⊢ s.piecewise f g =ᶠ[𝓝 x] f
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 ℕ∞
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
p : M ⊕ M'
⊢ ContinuousAt (Sum.elim f g) p ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g p)) ∘ Sum.elim f g ∘ ↑(extChartAt I p).symm) (range ↑I)
      (↑(extChartAt I p) p)

Tactic:
refine ⟨(Continuous.sumElim hf.continuous hg.continuous).continuousAt, ?_⟩

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
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
p : M ⊕ M'
⊢ ContDiffWithinAt 𝕜 n (↑(extChartAt J (Sum.elim f g p)) ∘ Sum.elim f g ∘ ↑(extChartAt I p).symm) (range ↑I)
    (↑(extChartAt I p) p)
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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst✝⁶] (s i)
⊢ ContMDiffOn I I' n f (⋃ i, s i)

Tactic:
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩

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 : ℕ∞ω
ι : Type u_11
s : ι → Set M
hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)
hs : ∀ (i : ι), IsOpen[inst✝⁶] (s i)
x : M
i : ι
hxsi : x ∈ (fun i ↦ s i) i
⊢ ContMDiffWithinAt I I' n f (⋃ i, s i) x
Module: Mathlib.Analysis.Normed.Operator.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : Nontrivial E
⊢ ‖fst 𝕜 E F‖ = 1

Tactic:
refine le_antisymm (norm_fst_le ..) ?_
  let ⟨e, he⟩ := exists_ne (0 : E)
  have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)
  rw [norm_zero, max_eq_left (norm_nonneg e)] at this
  rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]

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'
x : M
y : M'
n : ℕ∞ω
inst✝ : IsManifold I' n M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f univ x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x

Tactic:
continuousWithinAt_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'
x : M
y : M'
n : ℕ∞ω
inst✝ : IsManifold I' n M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) 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'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
n : ℕ∞ω
x : M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I' n M'
hx : x ∈ e.source
hy : f x ∈ e'.source
⊢ ContinuousWithinAt f univ x ∧
      ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' univ ∩ range ↑I)
        (↑(e.extend I) x) ↔
    ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (range ↑I) (↑(e.extend I) x)

Tactic:
continuousWithinAt_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'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
n : ℕ∞ω
x : M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I' n M'
hx : x ∈ e.source
hy : f x ∈ e'.source
⊢ ContinuousAt f x ∧
      ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' univ ∩ range ↑I)
        (↑(e.extend I) x) ↔
    ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (range ↑I) (↑(e.extend I) 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 x' : M
y : M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hx : x' ∈ (chartAt H x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f univ x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
continuousWithinAt_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'
x x' : M
y : M'
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hx : x' ∈ (chartAt H x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousAt f x' ∧
      ContDiffWithinAt 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
x : E
hx : x ∈ f.source
⊢ HasFDerivWithinAt (↑f) (f' x) f.source x

Tactic:
exact (hf' x hx).hasFDerivWithinAt

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'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑f y = ↑c'.symm (↑c' (↑f y))

Tactic:
by rw [c'.left_inv hy₁]

Goal state after: