awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
u : Set P
hu : IsOpen u
hne : u.Nonempty
⊢ ∃ s ⊆ u,
    AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) ∧
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) ⊤
have rcases : ∀ (x : P) (hx : x ∈ u),
  ∃ s ⊆ u,
    AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) ∧
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) ⊤
Tactic: rcases hne with ⟨x, hx⟩
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s ⊆ u,
    AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) ∧
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) ⊤
have rcases : ∀ (s : Set P) (hsu : s ⊆ u)
  (hs :
    AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) ∧
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) ⊤),
  ∃ s ⊆ u,
    AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s)) ∧
      Eq (α := AffineSubspace ℝ P) (affineSpan ℝ s) ⊤
Tactic: rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx)
    (singleton_nonempty _) (affineIndependent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
ι : Type u_3
inst_2 : Fintype ι
b : AffineBasis ι ℝ V
⊢ Membership.mem (γ := Set V)
    (interior ((convexHull ℝ : (a : Set V) → Set V) (range.{u_1, u_3 + 1} (ι := ι) (⇑b : (a : ι) → V))))
    (Finset.centroid.{0, u_1, u_1, u_3} ℝ (ι := ι) Finset.univ (⇑b : (a : ι) → V))
have this : Nonempty ι
Tactic: haveI := b.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s)) ↔
    Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
have refine : ∀ (h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤),
  Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
Tactic: refine ⟨affineSpan_eq_top_of_nonempty_interior, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
have obtain : ∀ (t : Set V) (hts : t ⊆ s) (b : AffineBasis (↑t : Type u_1) ℝ V)
  (hb : Eq (α := (a : (↑t : Type u_1)) → V) (⇑b : (a : (↑t : Type u_1)) → V) (Subtype.val (p := fun (x : V) ↦ x ∈ t))),
  Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
Tactic: obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis (↑t : Type u_1) ℝ V
hb : Eq (α := (a : (↑t : Type u_1)) → V) (⇑b : (a : (↑t : Type u_1)) → V) (Subtype.val (p := fun (x : V) ↦ x ∈ t))
this :
  Set.Nonempty.{u_1} (α := V)
    (interior ((convexHull ℝ : (a : Set V) → Set V) (range (ι := (↑t : Type u_1)) (⇑b : (a : (↑t : Type u_1)) → V))))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
have this₁ : Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) t))
Tactic: rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis (↑t : Type u_1) ℝ V
hb : Eq (α := (a : (↑t : Type u_1)) → V) (⇑b : (a : (↑t : Type u_1)) → V) (Subtype.val (p := fun (x : V) ↦ x ∈ t))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
have suffices : Set.Nonempty.{u_1} (α := V)
  (interior ((convexHull ℝ : (a : Set V) → Set V) (range (ι := (↑t : Type u_1)) (⇑b : (a : (↑t : Type u_1)) → V))))
Tactic: suffices (interior (convexHull ℝ (range b))).Nonempty by
    rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
    refine this.mono (by gcongr)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis (↑t : Type u_1) ℝ V
hb : Eq (α := (a : (↑t : Type u_1)) → V) (⇑b : (a : (↑t : Type u_1)) → V) (Subtype.val (p := fun (x : V) ↦ x ∈ t))
⊢ Set.Nonempty.{u_1} (α := V)
    (interior ((convexHull ℝ : (a : Set V) → Set V) (range (ι := (↑t : Type u_1)) (⇑b : (a : (↑t : Type u_1)) → V))))
have lift : ∀ (t : Finset V) (hts : (↑t : Set V) ⊆ s) (b : AffineBasis (↑(↑t : Set V) : Type u_1) ℝ V)
  (hb :
    Eq (α := (a : (↑(↑t : Set V) : Type u_1)) → V) (⇑b : (a : (↑(↑t : Set V) : Type u_1)) → V)
      (Subtype.val (p := fun (x : V) ↦ x ∈ (↑t : Set V)))),
  Set.Nonempty.{u_1} (α := V)
    (interior
      ((convexHull ℝ : (a : Set V) → Set V)
        (range (ι := (↑(↑t : Set V) : Type u_1)) (⇑b : (a : (↑(↑t : Set V) : Type u_1)) → V))))
Tactic: lift t to Finset V using b.finite_set
Cleared hypotheses: t, hts, b, hb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (interior s).Nonempty ↔ Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
have rw : (interior s).Nonempty ↔ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
Tactic: rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
rw : (interior s).Nonempty ↔ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
⊢ (interior s).Nonempty ↔ Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤
have rw₁ : (interior s).Nonempty ↔ (interior s).Nonempty
Tactic: rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
hv : v ≠ 0
⊢ asymptoticNhds ℝ P v ≤ cobounded P
have have : ∀ (p : P), asymptoticNhds ℝ P v ≤ cobounded P
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
hv : v ≠ 0
p : P
⊢ asymptoticNhds ℝ P v ≤ cobounded P
have rw : Tendsto (β := ℝ) ((fun (x : P) ↦ dist (id x) p) ∘ (fun (x : V) ↦ x +ᵥ p) ∘ fun (p : ℝ × V) ↦ p.1 • p.2)
  (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
Tactic: rw [← tendsto_id', ← Metric.tendsto_dist_right_atTop_iff p,
    asymptoticNhds_eq_smul_vadd v p, vadd_pure, ← map₂_smul, ← map_prod_eq_map₂, map_map,
    tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
hv : v ≠ 0
p : P
⊢ Tendsto (β := ℝ) ((fun (x : P) ↦ dist (id x) p) ∘ (fun (x : V) ↦ x +ᵥ p) ∘ fun (p : ℝ × V) ↦ p.1 • p.2)
    (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
have change : Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ dist (x.1 • x.2 +ᵥ p) p) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
Tactic: change Tendsto (fun x : ℝ × V => dist (x.1 • x.2 +ᵥ p) p) (atTop ×ˢ 𝓝 v) atTop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
v : V
hv : v ≠ 0
p : P
⊢ Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ dist (x.1 • x.2 +ᵥ p) p) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
have simp_rw : Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ ‖x.1‖ * ‖x.2‖) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
Tactic: simp_rw [dist_vadd_left, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Set P
hs : Bornology.IsBounded s
v : V
h : v ∈ asymptoticCone ℝ s
⊢ Membership.mem (γ := Set V) {0} v
have by_contra! : ∀ (hv : v ∉ {0}), False
Tactic: by_contra! hv
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
⊢ cobounded P = ⨆ (v : V), ⨆ (_ : Membership.mem (γ := Set V) (Metric.sphere 0 1) v), asymptoticNhds ℝ P v
have refine : cobounded P ≤ ⨆ (v : V), ⨆ (_ : Membership.mem (γ := Set V) (Metric.sphere 0 1) v), asymptoticNhds ℝ P v
Tactic: refine le_antisymm ?_ <| iSup₂_le fun _ h => asymptoticNhds_le_cobounded <|
    Metric.ne_of_mem_sphere h one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
hs :
  Membership.mem (γ := Filter P)
    (⨆ (v : V), ⨆ (_ : Membership.mem (γ := Set V) (Metric.sphere 0 1) v), asymptoticNhds ℝ P v) s
⊢ s ∈ cobounded P
have have : ∀ (p : P), s ∈ cobounded P
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
hs :
  Membership.mem (γ := Filter P)
    (⨆ (v : V), ⨆ (_ : Membership.mem (γ := Set V) (Metric.sphere 0 1) v), asymptoticNhds ℝ P v) s
p : P
⊢ s ∈ cobounded P
have hs₁ : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i),
  Membership.mem (γ := Filter P) (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul (α := Filter ℝ) atTop (𝓝 i))) s
Tactic: simp_rw [mem_iSup, asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
hs :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i),
    Membership.mem (γ := Filter P) (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul (α := Filter ℝ) atTop (𝓝 i))) s
⊢ s ∈ cobounded P
have choose! : ∀ (t : (i : V) → Set ℝ)
  (ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i))
  (u : (i : V) → Set V) (hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i)
  (smul_subset_s :
    ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s),
  s ∈ cobounded P
Tactic: choose! t ht u hu smul_subset_s using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
⊢ s ∈ cobounded P
have have : ∀ (cover : Finset V) (h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x)
  (h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)), s ∈ cobounded P
Tactic: have ⟨cover, h₁, h₂⟩ := (isCompact_sphere 0 1).elim_nhds_subcover u hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
⊢ s ∈ cobounded P
have rw : s ∈ comap (dist p) atTop
Tactic: rw [← Metric.comap_dist_left_atTop p]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
⊢ s ∈ comap (dist p) atTop
have refine : ∀ (x : P) (hx : x ∈ dist p ⁻¹' (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x)), x ∈ s
Tactic: refine ⟨Set.Ioi 0 ∩ ⋂ x ∈ cover, t x, inter_mem (Ioi_mem_atTop 0)
    (cover.iInter_mem_sets.mpr fun x hx => ht x (h₁ x hx)), fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : x ∈ dist p ⁻¹' (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x)
⊢ x ∈ s
have hx₁ : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
Tactic: rw [Set.mem_preimage, dist_eq_norm_vsub'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
have rw : ‖x'‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
rw : ‖x'‖ = 1
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
have rw₁ : ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
rw : ‖x'‖ = 1
rw₁ : ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
have rw₂ : ‖‖x -ᵥ p‖‖⁻¹ * ‖x -ᵥ p‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
rw : ‖x'‖ = 1
rw₁ : ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1
rw₂ : ‖‖x -ᵥ p‖‖⁻¹ * ‖x -ᵥ p‖ = 1
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
have rw₃ : ‖x -ᵥ p‖⁻¹ * ‖x -ᵥ p‖ = 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
rw : ‖x'‖ = 1
rw₁ : ‖‖x -ᵥ p‖⁻¹‖ * ‖x -ᵥ p‖ = 1
rw₂ : ‖‖x -ᵥ p‖‖⁻¹ * ‖x -ᵥ p‖ = 1
rw₃ : ‖x -ᵥ p‖⁻¹ * ‖x -ᵥ p‖ = 1
⊢ Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
have rw₄ : Eq (α := ℝ) 1 1
Tactic: rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
⊢ x ∈ s
have x'_mem : Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
Tactic: have x'_mem : x' ∈ Metric.sphere 0 1 := by
    rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hx.1.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AsymptoticCone (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
inst_4 : FiniteDimensional ℝ V
s : Set P
p : P
t : (i : V) → Set ℝ
ht : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), Membership.mem (γ := Filter ℝ) atTop (t i)
u : (i : V) → Set V
hu : ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), u i ∈ 𝓝 i
smul_subset_s :
  ∀ (i : V) (i_1 : Membership.mem (γ := Set V) (Metric.sphere 0 1) i), t i • u i ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, Membership.mem (γ := Set V) (Metric.sphere 0 1) x
h₂ : Subset.{u_1} (α := Set V) (Metric.sphere 0 1) (⋃ x ∈ cover, u x)
x : P
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x) ‖x -ᵥ p‖
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : Membership.mem (γ := Set V) (Metric.sphere 0 1) x'
⊢ x ∈ s
have have : ∀ (y : V) (y_mem : y ∈ cover) (hy : x' ∈ u y), x ∈ s
Tactic: have ⟨y, y_mem, hy⟩ := Set.mem_iUnion₂.mp (h₂ x'_mem)