mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : ContMDiffMul I n G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : ContMDiffMul I' n G'
f g : ContMDiffMonoidMorphism I I' n G G'
h : (fun a ↦ (↑a.toMonoidHom).toFun) f = (fun a ↦ (↑a.toMonoidHom).toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝¹⁰ : Monoid G
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : ContMDiffMul I n G
H' : Type u_5
inst✝⁶ : TopologicalSpace H'
E' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
G' : Type u_7
inst✝³ : Monoid G'
inst✝² : TopologicalSpace G'
inst✝¹ : ChartedSpace H' G'
inst✝ : ContMDiffMul I' n G'
g : ContMDiffMonoidMorphism I I' n G G'
toMonoidHom✝ : G →* G'
contMDiff_toFun✝ : ContMDiff I I' n (↑toMonoidHom✝).toFun
h :
  (fun a ↦ (↑a.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ } =
    (fun a ↦ (↑a.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, contMDiff_toFun := contMDiff_toFun✝ } = g
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
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert (↑(extChartAt I x) x)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))]
      ↑(extChartAt I x) x
hsub :
  v ⊆
    insert (↑(extChartAt I x) x)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) v
⊢ ↑(extChartAt I x).symm (↑(extChartAt I x) x) ∈ f ⁻¹' (extChartAt I' (f x)).source

Tactic:
by
      rw [extChartAt_to_inv]; apply mem_extChartAt_source

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Tactic:
refine ⟨(f.symm.continuousAt hX).continuousWithinAt, fun h2x => ?_⟩

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn (↑(chartAt H (↑f.symm X)) ∘ ↑f.symm ∘ ↑(chartAt H X).symm) (↑e.toPartialEquiv)
        (↑(chartAt H X).symm ⁻¹' f.symm.source ∩ e.source) ∧
      ↑(chartAt H X) X ∈ e.source
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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
x : M
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
hx : x ∈ e.source
hy : f x ∈ e'.source
⊢ MDiffAt[s] f x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)

Tactic:
rw [mdifferentiableWithinAt_iff_of_mem_maximalAtlas he he' hx hy, and_congr_right_iff]
  refine fun _ => differentiableWithinAt_congr_nhds ?_
  simp_rw [nhdsWithin_eq_iff_eventuallyEq, e.extend_symm_preimage_inter_range_eventuallyEq hs hx]

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

Goal state before:
pp: case mpr
𝕜 : 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 : ContinuousOn f s
⊢ (∀ (y : M'),
      ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            (↑𝓘(𝕜, E').toPartialEquiv ∘
              (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
            (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
              ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) →
    ∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
          f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
        (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
          ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))

Tactic:
· exact fun h' x y => (h' y).2 x 0

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

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

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

Tactic:
· rw [e₁.source_eq, e₂.source_eq]
    exact mapsTo_preimage _ _

Goal state after:
case refine_2
B : Type u_1
inst✝⁴ : TopologicalSpace B
F₁ : Type u_2
inst✝³ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝¹ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝ : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
f₁ : (TotalSpace (F₁ × F₂) fun x ↦ E₁ x × E₂ x) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun p ↦ ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ := fun p ↦ (↑e₁ p.1, ↑e₂ p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun p ↦ (p.1.1, p.1.2, p.2.2)
hf₁ : Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁
hf₂ : ContinuousOn f₂ (e₁.source ×ˢ e₂.source)
hf₃ : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f₃
⊢ EqOn (toFun' e₁ e₂) ((f₃ ∘ f₂) ∘ f₁) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
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 e' : OpenPartialHomeomorph (B × F) (B × F)),
    (∃ φ U,
        ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
          ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)) →
      e' ≈ e →
        ∃ φ U,
          ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
            ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
            e'.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)

Tactic:
rintro e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ hee'

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 e' : OpenPartialHomeomorph (B × F) (B × F)
φ : B → F ≃L[𝕜] F
U : Set B
hU : IsOpen[inst✝⁷] U
hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U
h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U
heφ : e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
hee' : e' ≈ e
⊢ ∃ φ U,
    ∃ (hU : IsOpen[inst✝⁷] U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U) (h2φ :
      ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
      e'.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
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 ∈ 𝓝 x
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I

Tactic:
← extChartAt_to_inv (I := I) x

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)}
⊢ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝[≠] ↑(extChartAt I x) x] ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ (Prod.fst ∘ fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x =
    (fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x

Tactic:
simp_rw [Function.comp, OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe]

Goal state after:
case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ ↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj) (f x)).1 = ↑(extChartAt IB (f x₀).proj) (f x).proj
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case sub1
𝕜 : 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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I ⊆
    ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I

pp: case sub2
𝕜 : 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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆
    ↑(extChartAt I' (f x)).symm ⁻¹' f '' s ∩ range ↑I'

Tactic:
case sub1 => mfld_set_tac

Goal state after:
case sub2
𝕜 : 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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆
    ↑(extChartAt I' (f x)).symm ⁻¹' f '' s ∩ range ↑I'
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
V : (x : E) → TangentSpace 𝓘(𝕜, E) x
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ ⟨x, V x⟩) x ↔ ContDiffAt 𝕜 n V x

Tactic:
simp only [← contMDiffWithinAt_univ, ← contDiffWithinAt_univ,
    contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

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

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
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
⊢ UniqueMDiffAt[TotalSpace.proj ⁻¹' s] p

Tactic:
by
  suffices UniqueMDiffAt[π F Z ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet)] p from
    this.mono (by simp)
  apply UniqueMDiffWithinAt.bundle_preimage_aux (hs.inter _) inter_subset_right
  exact (trivializationAt F Z p.proj).open_baseSet.mem_nhds
    (FiberBundle.mem_baseSet_trivializationAt' p.proj)

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f✝ f g : PartitionOfUnity ι X s
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f g : PartitionOfUnity ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝ i) x ≤ 1
h :
  { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
        sum_le_one' := sum_le_one'✝ }.toFun =
    g.toFun
⊢ { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
      sum_le_one' := sum_le_one'✝ } =
    g
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f✝ f g : BumpCovering ι X s
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ x ∈ s, ∃ i, ⇑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
        eventuallyEq_one' := eventuallyEq_one'✝ }.toFun =
    g.toFun
⊢ { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
      eventuallyEq_one' := eventuallyEq_one'✝ } =
    g
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
y : M
hy : y ∈ Set.univ
⊢ ⟨y, ∑ᶠ (i : ι), t i y⟩ = ⟨y, ∑' (i : ι), t i y⟩

Tactic:
rw [← tsum_eq_finsum (L := SummationFilter.unconditional ι)]

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
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
y : M
hy : y ∈ Set.univ
⊢ HasFiniteSupport fun i ↦ t i y