awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Structures (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ (Continuous (Y := 𝕜) fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∧
    ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
      ContDiffOn 𝕜 n
        ((↑(extChartAt 𝓘(𝕜, 𝕜) y) : 𝕜 → 𝕜) ∘
          (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∘
            (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜))
        ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
          (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜) ⁻¹'
            (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)
have refine : ∀ (x : 𝕜 × 𝕜) (y : 𝕜),
  ContDiffOn 𝕜 n
    ((↑(extChartAt 𝓘(𝕜, 𝕜) y) : 𝕜 → 𝕜) ∘
      (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∘ (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜))
    ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
      (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜) ⁻¹'
        (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)
Tactic: refine ⟨continuous_mul, fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Structures (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 n
    ((↑(extChartAt 𝓘(𝕜, 𝕜) y) : 𝕜 → 𝕜) ∘
      (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ∘ (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜))
    ((extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).target ∩
      (↑(extChartAt (ModelWithCorners.prod 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜)) x).symm : 𝕜 × 𝕜 → 𝕜 × 𝕜) ⁻¹'
        (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) ⁻¹' (extChartAt 𝓘(𝕜, 𝕜) y).source)
have simp : ContDiffOn 𝕜 (F := 𝕜) n (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) Set.univ
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Algebra.Structures (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
x : 𝕜 × 𝕜
y : 𝕜
⊢ ContDiffOn 𝕜 (F := 𝕜) n (fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2) Set.univ
have rw : ContDiff 𝕜 (F := 𝕜) n fun (p : 𝕜 × 𝕜) ↦ p.1 * p.2
Tactic: rw [contDiffOn_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Bordism (goal)
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
⊢ Continuous.{u, u_1} (Y := X) fun (x : M) ↦ ⋯.elim
have rw : ∀ (x : M), ContinuousAt.{u, u_1} (Y := X) (fun (x : M) ↦ sorry.elim) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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)
⊢ support (↑f : M → ℝ) =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
      (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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] (support (↑f : M → ℝ))
have rw : IsOpen[inst_3]
  ((OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source ∩
    (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut)
Tactic: rw [support_eq_inter_preimage]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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))
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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))
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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))
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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))
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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))
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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))
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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))
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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))
⊢ support (↑f : M → ℝ) =
    (↑(extChartAt I c).symm : E → M) '' (ball ((↑(extChartAt I c) : M → E) c) f.rOut ∩ range (↑I : H → E))
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.BumpFunction (goal)
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
⊢ support (↑f : M → ℝ) ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).source
have rw : (extChartAt I c).source ∩ (↑(extChartAt I c) : M → E) ⁻¹' ball ((↑(extChartAt I c) : M → E) c) f.rOut ⊆
  (extChartAt I c).source
Tactic: rw [f.support_eq_inter_preimage, ← extChartAt_source I]