awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M_1 : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I_1 : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M_1
inst_8 : ChartedSpace H M_1
inst_9 : IsManifold I_1 k M_1
inst_10 : CompactSpace M_1
inst_11 : BoundarylessManifold I_1 M_1
E' : Type u_7
H' : Type u_8
inst_12 : NormedAddCommGroup E'
inst_13 : NormedSpace ℝ E'
inst_14 : TopologicalSpace H'
M : Type u
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
I : ModelWithCorners ℝ E H
inst_17 : IsManifold I k M
inst_18 : IsEmpty M
⊢ ∀ (x : M), ContinuousAt.{u, u_1} (Y := X) (fun (x : M) ↦ ⋯.elim) x

Tactic:
fun x ↦ (IsEmpty.false x).elim

Premises used: False.elim, IsEmpty.false
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M_1 : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I_1 : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M_1
inst_8 : ChartedSpace H M_1
inst_9 : IsManifold I_1 k M_1
inst_10 : CompactSpace M_1
inst_11 : BoundarylessManifold I_1 M_1
E' : Type u_7
H' : Type u_8
inst_12 : NormedAddCommGroup E'
inst_13 : NormedSpace ℝ E'
inst_14 : TopologicalSpace H'
M : Type u
inst_15 : TopologicalSpace M
inst_16 : ChartedSpace H M
I : ModelWithCorners ℝ E H
inst_17 : IsManifold I k M
inst_18 : IsEmpty M
⊢ ∀ (x : M), ContinuousAt.{u, u_1} (Y := X) (fun (x : M) ↦ ⋯.elim) x

Tactic:
exact fun x ↦ (IsEmpty.false x).elim

Premises used: False.elim, IsEmpty.false
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
inst : TopologicalSpace X
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : IsManifold I k M
inst_8 : IsEmpty M
⊢ SingularManifold.M (k := k) (empty X M I) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
M : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : FiniteDimensional ℝ E
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I k M
inst_10 : CompactSpace M
inst_11 : BoundarylessManifold I M
E' : Type u_7
H' : Type u_8
inst_12 : NormedAddCommGroup E'
inst_13 : NormedSpace ℝ E'
inst_14 : TopologicalSpace H'
inst_15 : IsEmpty M
⊢ IsEmpty.{u_6 + 1} (SingularManifold.M (k := k) (empty X M I))

Tactic:
inferInstanceAs <| IsEmpty M

Premises used: _private.0.SingularManifold.instIsEmptyMEmpty._proof_1
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
inst : TopologicalSpace X
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
s : SingularManifold.{u_9, u_1, u_4, u_5} X k I
t : SingularManifold.{u_10, u_1, u_4, u_5} X k I
⊢ (s.sum t).M = Sum.{u_9, u_10} s.M t.M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Bordism
Goal:
X : Type u_1
inst : TopologicalSpace X
k : WithTop ℕ∞
E : Type u_4
H : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
s : SingularManifold.{u_9, u_1, u_4, u_5} X k I
t : SingularManifold.{u_10, u_1, u_4, u_5} X k I
⊢ (s.sum t).f = Sum.elim s.f t.f

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
inst_5 : FiniteDimensional ℝ E
c : M
f : SmoothBumpFunction I c
⊢ (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source.indicator
      ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E))

Tactic:
rfl

Premises used: SmoothBumpFunction.toFun, rfl
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
⊢ 0 < f.rOut

Tactic:
f.toContDiffBump.rOut_pos

Premises used: SmoothBumpFunction.toContDiffBump, ContDiffBump.rOut_pos
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
⊢ ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ⊆ (extChartAt I c).target

Tactic:
Subset.trans (inter_subset_inter_left _ ball_subset_closedBall) f.closedBall_subset

Premises used: Metric.ball_subset_closedBall, Set.Subset.trans, Set.inter_subset_inter_left, SmoothBumpFunction.closedBall_subset
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
⊢ ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) =
    ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ (extChartAt I c).target

Tactic:
(subset_inter inter_subset_left f.ball_subset).antisymm <| inter_subset_inter_right _ <|
    extChartAt_target_subset_range _

Premises used: Set.inter_subset_inter_right, SmoothBumpFunction.ball_subset, Set.inter_subset_left, extChartAt_target_subset_range, Set.subset_inter, HasSubset.Subset.antisymm
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ EqOn (↑f : M → ℝ) ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E))
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
eqOn_indicator

Premises used: Set.eqOn_indicator, SmoothBumpFunction.toFun
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
hx : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
⊢ (↑f : M → ℝ) =ᶠ[𝓝 x] (↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)

Tactic:
f.eqOn_source.eventuallyEq_of_mem <| (chartAt H c).open_source.mem_nhds hx

Premises used: chartAt, OpenPartialHomeomorph.open_source, SmoothBumpFunction.eqOn_source, Set.EqOn.eventuallyEq_of_mem, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
x : M
inst_5 : FiniteDimensional ℝ E
hs : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
hd : dist ((↑(extChartAt I c) : M → E) x) ((↑(extChartAt I c) : M → E) c) ≤ f.rIn
⊢ (↑f : M → ℝ) x = 1

Tactic:
simp only [f.eqOn_source hs, (· ∘ ·), f.one_of_mem_closedBall hd]

Premises used: Function.comp, SmoothBumpFunction.eqOn_source, SmoothBumpFunction.toContDiffBump, ContDiffBump.one_of_mem_closedBall
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
rw :
  support
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source.indicator
        ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E))) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
rw₁ :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      support ((↑f.toContDiffBump : E → ℝ) ∘ (↑(extChartAt I c) : M → E)) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
rw₂ :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' support (↑f.toContDiffBump : E → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
rw₃ :
  (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' support (↑f.toContDiffBump : E → ℝ) =
    (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
rw₄ :
  (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ support (↑f.toContDiffBump : E → ℝ)) =
    (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
rw₅ :
  (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ support (↑f.toContDiffBump : E → ℝ)) =
    (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ ball ((↑(extChartAt I c) : M → E) c) f.rOut)
rw₆ rw₇ :
  (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ ball ((↑(extChartAt I c) : M → E) c) f.rOut) =
    (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ ball ((↑(extChartAt I c) : M → E) c) f.rOut)
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut

Tactic:
rw [coe_def, support_indicator, support_comp_eq_preimage, ← extChartAt_source I,
    ← (extChartAt I c).symm_image_target_inter_eq', ← (extChartAt I c).symm_image_target_inter_eq',
    f.support_eq]

Premises used: Set.support_indicator, extChartAt, ContDiffBump.support_eq, extChartAt_source, Function.support_comp_eq_preimage, SmoothBumpFunction.toContDiffBump, PartialEquiv.symm_image_target_inter_eq', SmoothBumpFunction.coe_def
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
rw :
  IsOpen[inst_3]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut)
⊢ IsOpen[inst_3] (support (↑f : M → ℝ))

Tactic:
rw [support_eq_inter_preimage]

Premises used: SmoothBumpFunction.support_eq_inter_preimage
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ IsOpen[inst_3]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut)

Tactic:
isOpen_extChartAt_preimage c isOpen_ball

Premises used: isOpen_extChartAt_preimage, Metric.isOpen_ball
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ IsOpen[inst_3]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut)

Tactic:
exact isOpen_extChartAt_preimage c isOpen_ball

Premises used: isOpen_extChartAt_preimage, Metric.isOpen_ball
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
rw :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
rw₁ :
  (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
rw₂ :
  (↑(extChartAt I c).symm : E → M) '' ((extChartAt I c).target ∩ ball ((↑(extChartAt I c) : M → E) c) f.rOut) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
rw₃ :
  (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ (extChartAt I c).target) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
rw₄ rw₅ :
  (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ (extChartAt I c).target) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ (extChartAt I c).target)
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))

Tactic:
rw [f.support_eq_inter_preimage, ← extChartAt_source I,
    ← (extChartAt I c).symm_image_target_inter_eq', inter_comm,
    ball_inter_range_eq_ball_inter_target]

Premises used: extChartAt, SmoothBumpFunction.support_eq_inter_preimage, extChartAt_source, PartialEquiv.symm_image_target_inter_eq', Set.inter_comm, SmoothBumpFunction.ball_inter_range_eq_ball_inter_target
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
rw :
  (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut ⊆
    (extChartAt I c).source
⊢ support (↑f : M → ℝ) ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source

Tactic:
rw [f.support_eq_inter_preimage, ← extChartAt_source I]

Premises used: SmoothBumpFunction.support_eq_inter_preimage, extChartAt_source
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut ⊆
    (extChartAt I c).source

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
⊢ (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut ⊆
    (extChartAt I c).source

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hs : s ⊆ support (↑f : M → ℝ)
⊢ s ⊆ (extChartAt I c).source ∧ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut

Tactic:
rw [support_eq_inter_preimage, subset_inter_iff, ← extChartAt_source I, ← image_subset_iff] at hs

Premises used: Set.subset_inter_iff, SmoothBumpFunction.support_eq_inter_preimage, extChartAt_source, Set.image_subset_iff
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hs : s ⊆ (extChartAt I c).source ∧ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ s ⊆ (extChartAt I c).source

Tactic:
obtain ⟨hse, hsf⟩ := hs
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hs : s ⊆ (extChartAt I c).source ∧ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
hse : s ⊆ (extChartAt I c).source
⊢ (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut

Tactic:
obtain ⟨hse, hsf⟩ := hs
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
h₁ :
  (↑(extChartAt I c) : M → E) '' s ⊆
    closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s
h₂ :
  closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆
    (↑(extChartAt I c) : M → E) '' s
⊢ (↑(extChartAt I c) : M → E) '' s =
    closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ (↑(extChartAt I c) : M → E) '' s ⊆
    closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_

Premises used: Metric.ball_subset_closedBall, HasSubset.Subset.trans, Set.subset_inter
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
h₁ : (↑(extChartAt I c) : M → E) '' s ⊆ range (↑I : H → E)
h₂ : (↑(extChartAt I c) : M → E) '' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s
⊢ (↑(extChartAt I c) : M → E) '' s ⊆
    closedBall ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E) ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
refine subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_

Premises used: Metric.ball_subset_closedBall, HasSubset.Subset.trans, Set.subset_inter
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
x : M
⊢ (↑(extChartAt I c) : M → E) x ∈ range (↑I : H → E)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, ModelWithCorners.toFun'
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
x : M
⊢ (↑(extChartAt I c) : M → E) x ∈ range (↑I : H → E)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
h₁ : (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s
⊢ (↑(extChartAt I c) : M → E) '' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]

Premises used: extChartAt, PartialEquiv.image_eq_target_inter_inv_preimage
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Geometry.Manifold.BumpFunction
Goal:
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
c : M
f : SmoothBumpFunction I c
inst_5 : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : (↑(extChartAt I c) : M → E) '' s ⊆ ball ((↑(extChartAt I c) : M → E) c) f.rOut
⊢ (extChartAt I c).target ∩ (↑(extChartAt I c).symm : E → M) ⁻¹' s ⊆ (↑(extChartAt I c).symm : E → M) ⁻¹' s

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right