awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
inr :
  ∀
    (this :
      ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
        Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
          (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V))
    (hx₀ : ¬0 < x),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have wlog : ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
  Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
Tactic: wlog hx₀ : 0 < x generalizing x U
Cleared hypotheses: U, hU, hU₀, x, hxU
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
hx₀ : ¬0 < x
⊢ 0 < -x
have hx₁ : x = 0 ∨ 0 < -x
Tactic: rw [not_lt, le_iff_eq_or_lt, ← neg_pos] at hx₀
Cleared hypotheses: hx₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
hx₀ : ¬0 < x
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have hx₁ : 0 < -x
Tactic: replace hx₀ : 0 < -x := by
      rw [not_lt, le_iff_eq_or_lt, ← neg_pos] at hx₀
      exact hx₀.resolve_left <| ne_of_mem_of_not_mem hxU hU₀
Cleared hypotheses: hx₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
hx₀ : 0 < -x
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have this₁ : Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (-x) (↑y : E)))
  (-U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
Tactic: specialize this hU.neg (by simpa) (-x) (by simpa) hx₀
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
hx₀ : 0 < -x
this :
  Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (-x) (↑y : E)))
    (-U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have this₁ : Neg.neg ⁻¹' (-(U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)) ∈ 𝓝 (x • (↑y : E))
Tactic: simp only [neg_smul, nhds_neg, Set.neg_smul, Filter.mem_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have hr₀ : 0 < r
Tactic: have hr₀ : 0 < r := lt_of_le_of_ne (by simpa using norm_nonneg y.1) hr.symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
hr₀ : 0 < r
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) x (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have lift : ∀ (x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }) (hxU : (↑x : ℝ) ∈ U),
  Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
Tactic: lift x to Ioi (0 : ℝ) using hx₀
Cleared hypotheses: x, hxU, hx₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have this : SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈ 𝓝 (y, x)
Tactic: have : V ×ˢ (Ioi (0 : ℝ) ↓∩ U) ∈ 𝓝 (y, x) :=
    prod_mem_nhds (hV.mem_nhds hyV) (hU.preimage_val.mem_nhds hxU)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this : SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈ 𝓝 (y, x)
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have this₁ : Membership.mem (γ := Filter E)
  (map
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
        (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
    (𝓝 (y, x)))
  (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
        (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
    SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
Tactic: replace := image_mem_map (m := Subtype.val ∘ (homeomorphSphereProd E r hr₀).symm) this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (map
      (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
      (𝓝 (y, x)))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have rw : ∀
  (this :
    Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
          (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
            (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
        SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
      𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))),
  Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
Tactic: rw [← Filter.map_map, (homeomorphSphereProd _ r hr₀).symm.map_nhds_eq,
    map_nhds_subtype_val, IsOpen.nhdsWithin_eq, homeomorphSphereProd_symm_apply_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (map
      (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
      (𝓝 (y, x)))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
rw :
  ∀
    (this :
      Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
          SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
        𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have h : ∀
  (this :
    Membership.mem (γ := Filter E)
      (𝓝[{0}ᶜ]
        (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
                (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
              (y, x)) :
          E))
      (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
          (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
            (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
        SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))),
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ
Tactic: rw [← Filter.map_map, (homeomorphSphereProd _ r hr₀).symm.map_nhds_eq,
    map_nhds_subtype_val, IsOpen.nhdsWithin_eq, homeomorphSphereProd_symm_apply_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
      (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
          (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
            (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
        SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
      a →
    a ∈ U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
Tactic: filter_upwards [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
⊢ Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
      (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
        (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
      (a, b) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
have h : (↑(a, b).2 : ℝ) • (↑(a, b).1 : E) ∈ U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
Tactic: rw [Function.comp_apply, homeomorphSphereProd_symm_apply_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
⊢ (↑(a, b).2 : ℝ) • (↑(a, b).1 : E) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
have h : (↑(a, b).2 : ℝ) ∈ U
Tactic: apply Set.smul_mem_smul
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.RadialEquiv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
    𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
h : (↑(a, b).2 : ℝ) ∈ U
⊢ (↑(a, b).2 : ℝ) • (↑(a, b).1 : E) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
have h₁ : (↑(a, b).1 : E) ∈ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
Tactic: apply Set.smul_mem_smul
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
⊢ LinearIndependent 𝕜 (↑b : β → X)
have refine : ∀ (l : β →₀ 𝕜)
  (hl : Eq.{u_2 + 1} (α := X) ((Finsupp.linearCombination 𝕜 (↑b : β → X) : (a : β →₀ 𝕜) → X) l : X) (0 : X)) (a : β),
  Eq.{u_1 + 1} (α := 𝕜) ((l : (a : β) → 𝕜) a : 𝕜) ((0 : (a : β) → 𝕜) a : 𝕜)
Tactic: refine linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
⊢ LinearIndependent 𝕜 (↑b : β → X)
have refine : ∀ (l : β →₀ 𝕜)
  (hl : Eq.{u_2 + 1} (α := X) ((Finsupp.linearCombination 𝕜 (↑b : β → X) : (a : β →₀ 𝕜) → X) l : X) (0 : X)) (a : β),
  Eq.{u_1 + 1} (α := 𝕜) ((l : (a : β) → 𝕜) a : 𝕜) ((0 : (a : β) → 𝕜) a : 𝕜)
Tactic: classical
  refine linearIndependent_iff.mpr (fun l hl ↦ l.ext ?_)
  simpa [l.linearCombination_apply, Finsupp.sum, b.ortho, Pi.single_apply] using
    fun i ↦ congr_arg (b.coord i) hl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ (↑(b.proj A) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))
have a : (↑(b.proj A) : X →ₗ[𝕜] X).range ≤ Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
a : (↑(b.proj A) : X →ₗ[𝕜] X).range ≤ Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))
⊢ (↑(b.proj A) : X →ₗ[𝕜] X).range = Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β))
have a₁ : Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)) ≤ (↑(b.proj A) : X →ₗ[𝕜] X).range
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ Membership.mem (α := X) (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
    (((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) x : X)
have a : Membership.mem (γ := Submodule 𝕜 X) (Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)))
  (∑ i ∈ A, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((b.coord i : (a : X) → 𝕜) x : 𝕜) ((↑b : β → X) i))
Tactic: rw [ContinuousLinearMap.coe_coe, proj_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
⊢ Submodule.span 𝕜 ((↑b : β → X) '' (↑A : Set β)) ≤ (↑(b.proj A) : X →ₗ[𝕜] X).range
have a : (↑b : β → X) '' (↑A : Set β) ⊆ (↑(↑(b.proj A) : X →ₗ[𝕜] X).range : Set X)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
⊢ (↑b : β → X) i ∈ (↑(↑(b.proj A) : X →ₗ[𝕜] X).range : Set X)
have h : ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
Tactic: use b i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Bases (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
X : Type u_2
inst_1 : NormedAddCommGroup X
inst_2 : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
i : β
hi : i ∈ (↑A : Set β)
⊢ ((↑(b.proj A) : X →ₗ[𝕜] X) : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
have h : (b.proj A : (a : X) → X) ((↑b : β → X) i) = (↑b : β → X) i
Tactic: rw [ContinuousLinearMap.coe_coe, proj_apply_basis_mem, if_pos (Finset.mem_coe.mp hi)]