mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
⊢ ‖B - A‖ ≤ ↑(min δ δ'') → |B.det - A.det| ≤ ↑ε

Tactic:
hB

Goal state after:
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑(min δ δ'')
⊢ |B.det - A.det| ≤ ↑ε
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑(min δ δ'')
⊢ dist B.det A.det ≤ ↑ε

Tactic:
apply (hδ' B _).le

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := ⋯
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑(min δ δ'')
⊢ dist B A < δ'
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✝ : DiscreteTopology H
x : M
this : IsOpen[inst✝²] ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ (chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x} ⊆ {x}

Tactic:
simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]

Goal state after:
H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : DiscreteTopology H
x : M
this : IsOpen[inst✝²] ((chartAt H x).source ∩ ↑(chartAt H x) ⁻¹' {↑(chartAt H x) x})
⊢ ∀ y ∈ (chartAt H x).source, ↑(chartAt H x) y = ↑(chartAt H x) x → y = x
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: case inl
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M
⊢ Sum.inl x ∈ Sum.inl '' (ChartedSpace.chartAt x).source

Tactic:
← OpenPartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inl

Goal state after:
case inl
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✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
x : M
⊢ Sum.inl x ∈ ((ChartedSpace.chartAt x).lift_openEmbedding ⋯).source
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : e ∈ StructureGroupoid.maximalAtlas M G
he' : e' ∈ atlas H M
s : Set M
hs : IsOpen[inst✝²] s
⊢ e'.symm ≫ₕ e.restr s ∈ G

Tactic:
by
  have hs'' : IsOpen (e' '' (e'.source ∩ s)) := by
    rw [isOpen_image_iff_of_subset_source e' inter_subset_left]
    exact e'.open_source.inter hs
  have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
  exact G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').2 ht) (e.symm_trans_restr e' hs)

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
⊢ ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε

Tactic:
hB

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ |B.det - A.det| ≤ ↑ε
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ dist B.det A.det ≤ ↑ε

Tactic:
apply (hδ' B _).le

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ dist B A < δ'
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'
P : (H → H') → Set H → H → Prop
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ ContinuousWithinAt (Subtype.val ∘ f) s x ↔ ContinuousWithinAt f s x

pp: case refine_2
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
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ P (↑(chartAt H' ((Subtype.val ∘ f) x)) ∘ (Subtype.val ∘ f) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
      (↑(chartAt H x) x) ↔
    P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

Tactic:
· exact Topology.IsEmbedding.subtypeVal.isInducing.continuousWithinAt_iff.symm

Goal state after:
case refine_2
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
U : Opens M'
f : M → ↥U
s : Set M
x : M
⊢ P (↑(chartAt H' ((Subtype.val ∘ f) x)) ∘ (Subtype.val ∘ f) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s)
      (↑(chartAt H x) x) ↔
    P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr.refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
B : E →L[ℝ] E
⊢ ‖B - A‖ ≤ ↑(min δ δ'') → |B.det - A.det| ≤ ↑ε

Tactic:
hB

Goal state after:
case inr.refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : ↑m < ENNReal.ofReal |A.det|
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
δpos : 0 < δ
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑(min δ δ'')
⊢ |B.det - A.det| ≤ ↑ε
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
⊢ ContinuousAt f ↑x ↔ ContinuousAt (f ∘ Subtype.val) x

Tactic:
U.isOpenEmbedding'.continuousAt_iff

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

Goal state before:
pp: case refine_2
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
⊢ P (↑(chartAt H' (f ↑x)) ∘ f ∘ ↑(chartAt H ↑x).symm) (↑(chartAt H ↑x).symm ⁻¹' univ) (↑(chartAt H ↑x) ↑x) ↔
    P (↑(chartAt H' ((f ∘ Subtype.val) x)) ∘ (f ∘ Subtype.val) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' univ)
      (↑(chartAt H x) x)

Tactic:
apply hG.congr_iff
    exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)

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

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

Tactic:
exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

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

Goal state before:
pp: case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ ContDiffOn 𝕜 n (↑(I.prod I') ∘ ↑(e.prod e').symm ∘ ↑(I.prod I').symm)
    (↑(I.prod I').symm ⁻¹' (e.prod e'.toPartialEquiv).target ∩ range ↑(I.prod I'))

Tactic:
have h3 := ContDiffOn.prodMap he_symm he'_symm
    rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
    rw [← (I.prod I').image_eq]
    exact h3

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst✝¹] ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' s)

Tactic:
by
  rw [← extChartAt_source I]
  exact isOpen_extChartAt_preimage' x hs

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
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_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
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 : M → M'
x : M
n : WithTop ℕ∞
g : N → N'
y : N
hf : ContMDiffAt I I' n f x
hg : ContMDiffAt J J' n g y
⊢ ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (x, y)

Tactic:
by
  simp only [← contMDiffWithinAt_univ, ← univ_prod_univ] at *
  exact hf.prodMap hg

Goal state after:
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
⊢ 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:
have : ContDiffWithinAt 𝕜 n ((extChartAt J (f x)) ∘ f ∘ (extChartAt I x).symm)
        (range I) ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) := by
      let hf' := hf x
      rw [contMDiffAt_iff] at hf'
      simpa using hf'.2
    apply this.congr_of_eventuallyEq
    · simp only [extChartAt, Sum.elim_inl, ChartedSpace.sum_chartAt_inl]
      filter_upwards with a
      congr
    · -- They agree at the image of x.
      simp only [extChartAt, ChartedSpace.sum_chartAt_inl, Sum.elim_inl]
      congr

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

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
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
M' : Type u_7
inst✝ : TopologicalSpace M'
f : M → M'
s : Set M
x : M
h : ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) (s ∩ (extChartAt I x).source) x
⊢ ContinuousWithinAt f (s ∩ (extChartAt I x).source) x

Tactic:
apply this.congr

Goal state after:
case refine_2.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_7
inst✝ : TopologicalSpace M'
f : M → M'
s : Set M
x : M
h : ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) (s ∩ (extChartAt I x).source) x
⊢ ∀ y ∈ s ∩ (extChartAt I x).source, f y = ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) y

case refine_2.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_7
inst✝ : TopologicalSpace M'
f : M → M'
s : Set M
x : M
h : ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
this : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) (s ∩ (extChartAt I x).source) x
⊢ f x = ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x)) x
Module: Mathlib.Geometry.Manifold.MFDeriv.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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I
this : ContDiffWithinAt 𝕜 1 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))
⊢ DifferentiableWithinAt 𝕜 (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' ↑e.symm ⁻¹' s ∩ range ↑I) (↑I (↑e x))

Tactic:
convert! (h.comp' _ (this.differentiableWithinAt one_ne_zero)).mono_of_mem_nhdsWithin _
        using 1

Goal state after:
case e'_11
𝕜 : 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_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I
this : ContDiffWithinAt 𝕜 1 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))
⊢ ↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm = (↑I' ∘ f ∘ ↑I.symm) ∘ ↑I ∘ ↑e.symm ∘ ↑I.symm

case convert_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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I
this : ContDiffWithinAt 𝕜 1 (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))
⊢ ↑I.symm ⁻¹' e.target ∩ range ↑I ∩ ↑I ∘ ↑e.symm ∘ ↑I.symm ⁻¹' (↑I.symm ⁻¹' s ∩ range ↑I) ∈
    𝓝[↑I.symm ⁻¹' ↑e.symm ⁻¹' s ∩ range ↑I] ↑I (↑e x)
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ ContMDiff I' I n fun x ↦ ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
by
  simp only [← finprod_subtype_eq_finprod_cond]
  exact contMDiff_finprod (fun i ↦ hc i i.2) (hf.comp_injective Subtype.coe_injective)

Goal state after: