awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
h :
  ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((fun (p : H × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) p.1, id p.2))
            ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)))).proj
      (E := Z) =
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)
⊢ ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((fun (p : H × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) p.1, id p.2))
            ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)))).proj
      (E := Z) ∈
    s

Tactic:
convert! hz.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
h :
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)).1 ∈
    Trivialization.baseSet (trivializationAt F Z x)
⊢ ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((fun (p : H × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) p.1, id p.2))
            ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)))).proj
      (E := Z) =
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)

Tactic:
apply Trivialization.proj_symm_apply'

Premises used: Bundle.Trivialization.proj_symm_apply'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)).1 ∈
    Trivialization.baseSet (trivializationAt F Z x)

Tactic:
h's hz.1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)).1 ∈
    Trivialization.baseSet (trivializationAt F Z x)

Tactic:
exact h's hz.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
right :
  ∀ (u : H)
    (hz :
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) ((↑I : H → E) u)) ∈ s ∧
        ∃ (y : H), (↑I : H → E) y = (↑I : H → E) u),
    ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = ((↑I : H → E) u, w)
⊢ ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)

Tactic:
rcases hz.2 with ⟨u, rfl⟩

Premises used: And.right, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
w : F
u : H
hz :
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) ((↑I : H → E) u)) ∈ s ∧
    ∃ (y : H), (↑I : H → E) y = (↑I : H → E) u
⊢ ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = ((↑I : H → E) u, w)

Tactic:
⟨(u, w), rfl⟩

Premises used: Prod.mk, Exists.intro, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
w : F
u : H
hz :
  (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) ((↑I : H → E) u)) ∈ s ∧
    ∃ (y : H), (↑I : H → E) y = (↑I : H → E) u
⊢ ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = ((↑I : H → E) u, w)

Tactic:
exact ⟨(u, w), rfl⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
this :
  UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))))) p
⊢ Subset (α := Set (TotalSpace F Z))
    (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z)))))
    (TotalSpace.proj (E := Z) ⁻¹' s)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
suffices :
  UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))))) p
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p

Tactic:
suffices UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (π F Z ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet)) p from this.mono (by simp)
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
apply : Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))) ∈ nhds (p.proj (E := Z))
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))))) p

Tactic:
apply UniqueMDiffWithinAt.bundle_preimage_aux (hs.inter _) inter_subset_right

Premises used: UniqueMDiffWithinAt.inter, _private.0.UniqueMDiffWithinAt.bundle_preimage_aux, Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
⊢ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))) ∈ nhds (p.proj (E := Z))

Tactic:
IsOpen.mem_nhds (trivializationAt F Z p.proj).open_baseSet
    (FiberBundle.mem_baseSet_trivializationAt' p.proj)

Premises used: FiberBundle.mem_baseSet_trivializationAt', Bundle.Trivialization.open_baseSet, Bundle.TotalSpace.proj, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
⊢ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))) ∈ nhds (p.proj (E := Z))

Tactic:
exact IsOpen.mem_nhds (trivializationAt F Z p.proj).open_baseSet
    (FiberBundle.mem_baseSet_trivializationAt' p.proj)

Premises used: FiberBundle.mem_baseSet_trivializationAt', Bundle.Trivialization.open_baseSet, Bundle.TotalSpace.proj, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
b : M
hs : UniqueMDiffWithinAt I s b
x : Z b
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (M := TotalSpace F Z) (TotalSpace.proj (E := Z) ⁻¹' s) ⟨b, x⟩

Tactic:
hs.bundle_preimage (p := ⟨b, x⟩)

Premises used: UniqueMDiffWithinAt.bundle_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn (I.prod 𝓘(𝕜, F)) (M := TotalSpace F Z) (TotalSpace.proj (E := Z) ⁻¹' s)

Tactic:
fun _p hp ↦
  (hs _ hp).bundle_preimage

Premises used: UniqueMDiffOn, Bundle.TotalSpace.proj, UniqueMDiffWithinAt.bundle_preimage
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
⊢ LocallyCompactSpace H

Tactic:
haveI := I.locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
haveI := ChartedSpace.locallyCompactSpace H M
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ SecondCountableTopology H

Tactic:
haveI := I.secondCountableTopology
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this : SecondCountableTopology H
⊢ SecondCountableTopology M

Tactic:
haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
⊢ MetrizableSpace M

Tactic:
metrizableSpace_of_t3_secondCountable M

Premises used: TopologicalSpace.metrizableSpace_of_t3_secondCountable
-- Module: Mathlib.Geometry.Manifold.Metrizable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
⊢ MetrizableSpace M

Tactic:
exact metrizableSpace_of_t3_secondCountable M

Premises used: TopologicalSpace.metrizableSpace_of_t3_secondCountable
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
s_1 : Set M
f_1 : SmoothPartitionOfUnity ι I M s_1
n : ℕ∞
s : Set M
f g : SmoothPartitionOfUnity ι I M s
h : f.toFun (s := s) = g.toFun (s := s)
mk :
  ∀ (toFun : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
    (locallyFinite' : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : M) → ℝ))
    (nonneg' : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun i : (a : M) → ℝ) x : ℝ))
    (sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1)
    (sum_le_one' : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1)
    (h :
      (SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
        g.toFun (s := s)),
    SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
s_1 : Set M
f : SmoothPartitionOfUnity ι I M s_1
n : ℕ∞
s : Set M
g : SmoothPartitionOfUnity ι I M s
toFun : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite' : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : M) → ℝ)
nonneg' : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun i : (a : M) → ℝ) x : ℝ)
sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
sum_le_one' : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
h :
  (SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
    g.toFun (s := s)
mk :
  ∀ (toFun_1 : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
    (locallyFinite'_1 : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : M) → ℝ))
    (nonneg'_1 : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun_1 i : (a : M) → ℝ) x : ℝ))
    (sum_eq_one'_1 : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1)
    (sum_le_one'_1 : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1)
    (h :
      (SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
        (SmoothPartitionOfUnity.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1).toFun (s :=
          s)),
    SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' =
      SmoothPartitionOfUnity.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1
⊢ SmoothPartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g

Tactic:
cases g
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
s_1 : Set M
f : SmoothPartitionOfUnity ι I M s_1
n : ℕ∞
s : Set M
toFun : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite' : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : M) → ℝ)
nonneg' : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun i : (a : M) → ℝ) x : ℝ)
sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
sum_le_one' : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
toFun_1 : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'_1 : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : M) → ℝ)
nonneg'_1 : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun_1 i : (a : M) → ℝ) x : ℝ)
sum_eq_one'_1 : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1
sum_le_one'_1 : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1
h :
  (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
    (mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1).toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' =
    mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦
    support (M := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)

Tactic:
f.locallyFinite'

Premises used: SmoothPartitionOfUnity.locallyFinite'
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
i : ι
x : M
⊢ LE.le (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)

Tactic:
f.nonneg' i x

Premises used: SmoothPartitionOfUnity.nonneg'