mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ contDiffGroupoid 0 I = continuousGroupoid H

Tactic:
apply le_antisymm le_top
  intro u _
  -- we have to check that every open partial homeomorphism belongs to `contDiffGroupoid 0 I`,
  -- by unfolding its definition
  change u ∈ contDiffGroupoid 0 I
  rw [contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid]
  simp only [contDiffOn_zero]
  constructor
  · refine I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm ?_)
    exact (mapsTo_preimage _ _).mono_left inter_subset_left
  · refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
    exact (mapsTo_preimage _ _).mono_left inter_subset_left

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

Goal state before:
pp: case refine_3
𝕜 : 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'
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
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : ℕ∞ω
t : Set M'
g : M' → M''
x : M
st : MapsTo f s t
e : PartialEquiv M E := extChartAt I x
e' : PartialEquiv M' E' := extChartAt I' (f x)
hg :
  ContinuousWithinAt g t (f x) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' t ∩ range ↑I')
      (writtenInExtChartAt I I' x f (↑e x))
hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑e' ∘ f ∘ ↑e.symm) (↑e.symm ⁻¹' s ∩ range ↑I) (↑e x)
this : ↑e' (f x) = writtenInExtChartAt I I' x f (↑e x)
A : ∀ᶠ (y : E) in 𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x, f (↑e.symm y) ∈ t ∧ f (↑e.symm y) ∈ e'.source
⊢ (↑(extChartAt I'' ((g ∘ f) x)) ∘ (g ∘ f) ∘ ↑e.symm) (↑e x) =
    ((↑(extChartAt I'' (g (f x))) ∘ g ∘ ↑e'.symm) ∘ writtenInExtChartAt I I' x f) (↑e x)

Tactic:
· simp only [e, e', writtenInExtChartAt, (· ∘ ·), mem_extChartAt_source,
      e.left_inv, e'.left_inv]

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
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiffAt I 𝓘(𝕜, F₁ × F₂) n f x ↔
    ContMDiffAt I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) x ∧ ContMDiffAt I 𝓘(𝕜, F₂) n (Prod.snd ∘ f) x

Tactic:
by
  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
  exact contMDiffAt_prod_iff f

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

Goal state before:
pp: case hd
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
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ Pairwise (Disjoint on fun n ↦ s ∩ u n)

Tactic:
exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Goal state after:
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'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (fun x ↦ extend Subtype.val f 1 ↑x) x

Tactic:
simp_rw [← comp_def]

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'
inst✝¹ : T2Space M
inst✝ : One M'
n : ℕ∞ω
U : Opens M
f : ↥U → M'
supp : HasCompactMulSupport f
diff : ContMDiff I I' n f
x✝ : M
x : ↥U
h : ↑x ∈ mulTSupport (extend Subtype.val f 1)
⊢ ContMDiffAt I I' n (extend Subtype.val f 1 ∘ Subtype.val) x
Module: Mathlib.Geometry.Manifold.MFDeriv.Defs

Goal state before:
pp: case ht
𝕜 : 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 g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : DifferentiableWithinAtProp I I' f s x
⊢ ∀ x ∈ ↑I.symm ⁻¹' s ∩ range ↑I, (↑I' ∘ g ∘ ↑I.symm) x = (↑I' ∘ f ∘ ↑I.symm) x

pp: case 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
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 g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : DifferentiableWithinAtProp I I' f s x
⊢ (↑I' ∘ g ∘ ↑I.symm) (↑I x) = (↑I' ∘ f ∘ ↑I.symm) (↑I x)

Tactic:
· intro y hy
        simp only [mfld_simps] at hy
        simp only [h, hy, mfld_simps]

Goal state after:
case 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
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 g : H → H'
h : ∀ y ∈ s, f y = g y
hx : f x = g x
hf : DifferentiableWithinAtProp I I' f s x
⊢ (↑I' ∘ g ∘ ↑I.symm) (↑I x) = (↑I' ∘ f ∘ ↑I.symm) (↑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'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffOn I I' n f s
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
⊢ w ∈ s

Tactic:
simp only [w, hz, mfld_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : ContMDiffWithinAt I I' n f s w
this : w ∈ s
⊢ w ∈ (chartAt H x).source

Tactic:
simp only [w, hz, mfld_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : ContMDiffWithinAt I I' n f s w
this : w ∈ s
w1 : w ∈ (chartAt H x).source
⊢ f w ∈ (chartAt H' y).source

Tactic:
simp only [w, hz, mfld_simps]

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

Goal state before:
pp: case e'_12
𝕜 : 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
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : ContMDiffWithinAt I I' n f s w
this : w ∈ s
w1 : w ∈ (chartAt H x).source
w2 : f w ∈ (chartAt H' y).source
⊢ z = ↑(extChartAt I x) w

Tactic:
simp only [w, hz, mfld_simps]

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 : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
smul_eq_mul

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ MDiffAt[s] f x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
by
  simp only [mdifferentiableWithinAt_iff', mfld_simps]
  exact ⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, 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'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
h : MDiff[s] f
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
⊢ w ∈ s

Tactic:
simp only [w, hz, mfld_simps]

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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : MDiffAt[s] f w
this : w ∈ s
⊢ w ∈ (chartAt H x).source

Tactic:
simp only [w, hz, mfld_simps]

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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : MDiffAt[s] f w
this : w ∈ s
w1 : w ∈ (chartAt H x).source
⊢ f w ∈ (chartAt H' y).source

Tactic:
simp only [w, hz, mfld_simps]

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

Goal state before:
pp: case e'_13
𝕜 : 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
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range ↑I ∧ ↑I.symm z ∈ (chartAt H x).target) ∧
    ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ f (↑(chartAt H x).symm (↑I.symm z)) ∈ (chartAt H' y).source
w : M := ↑(extChartAt I x).symm z
h : MDiffAt[s] f w
this : w ∈ s
w1 : w ∈ (chartAt H x).source
w2 : f w ∈ (chartAt H' y).source
⊢ z = ↑(extChartAt I x) w

Tactic:
simp only [w, hz, mfld_simps]

Goal state after:
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✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
y : E b
⊢ (Pretrivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
coe_linearMapAt

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
y : E b
⊢ (fun y ↦ if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0) y =
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
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✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
y : E b
⊢ (Trivialization.linearMapAt R e b) y = if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0

Tactic:
coe_linearMapAt

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
y : E b
⊢ (fun y ↦ if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0) y =
    if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
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
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm z ∈ {x}ᶜ

Tactic:
push _ ∈ _ at h'z ⊢

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
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).symm z = x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((extChartAt IB x.proj).prod (PartialEquiv.refl F)).target ∩
      ↑((extChartAt IB x.proj).prod (PartialEquiv.refl F)).symm ⁻¹' (trivializationAt F E x.proj).target =
    ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ

Tactic:
Trivialization.target_eq,

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((extChartAt IB x.proj).prod (PartialEquiv.refl F)).target ∩
      ↑((extChartAt IB x.proj).prod (PartialEquiv.refl F)).symm ⁻¹' (trivializationAt F E x.proj).baseSet ×ˢ univ =
    ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source

Tactic:
· apply inter_subset_left

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x).symm y ∈ (chartAt H x).source

Tactic:
← extChartAt_source (I := I)

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
Module: Mathlib.Geometry.Manifold.MFDeriv.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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x).symm y ∈ (chartAt H x).source

Tactic:
← extChartAt_source (I := I)

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ ↑(extChartAt I x).symm y ∈ (extChartAt I x).source