awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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 : 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:
⟨s, hsu, hs⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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 : 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:
exact ⟨s, hsu, hs⟩
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ u) ⊤

Tactic:
let ⟨_, hsu, _, hs'⟩ := hu.exists_subset_affineIndependent_span_eq_top hne
  top_unique <| hs' ▸ affineSpan_mono _ hsu

Premises used: IsOpen.exists_subset_affineIndependent_span_eq_top, Real, Eq.rec, affineSpan, top_unique, _private.0.IsOpen.affineSpan_eq_top.match_1, affineSpan_mono, Top.top, Eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
s : Set V
hs : Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
⊢ Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤

Tactic:
top_unique <| isOpen_interior.affineSpan_eq_top hs ▸
    (affineSpan_mono _ interior_subset).trans_eq (affineSpan_convexHull _)

Premises used: LE.le.trans_eq, interior_subset, isOpen_interior, affineSpan_convexHull, Eq.rec, top_unique, affineSpan_mono, IsOpen.affineSpan_eq_top
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
ι : Type u_3
inst_2 : Fintype ι
b : AffineBasis ι ℝ V
⊢ Nonempty ι

Tactic:
haveI := b.nonempty
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
ι : Type u_3
inst_2 : Fintype ι
b : AffineBasis ι ℝ V
this : Nonempty ι
⊢ 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))

Tactic:
simp only [b.interior_convexHull, mem_setOf_eq, b.coord_apply_centroid (Finset.mem_univ _),
    inv_pos, Nat.cast_pos, Finset.card_pos, Finset.univ_nonempty, forall_true_iff]

Premises used: Finset.mem_univ, Nat.cast_pos, AffineBasis.interior_convexHull, Finset.univ_nonempty, inv_pos, Set.mem_setOf_eq, AffineBasis.coord_apply_centroid, Finset.card_pos, forall_true_iff
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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) ⊤

Tactic:
⟨affineSpan_eq_top_of_nonempty_interior, fun h => ?_⟩

Premises used: affineSpan_eq_top_of_nonempty_interior, Iff.intro
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : FiniteDimensional ℝ V
s : Set V
refine :
  ∀ (h : Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤),
    Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s)) ↔
    Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤

Tactic:
refine ⟨affineSpan_eq_top_of_nonempty_interior, fun h => ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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) ⊤
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))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))

Tactic:
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h

Premises used: AffineBasis.exists_affine_subbasis
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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) t))

Tactic:
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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) t))
⊢ Subset.{u_1} (α := Set V) (interior ((convexHull ℝ : (a : Set V) → Set V) t))
    (interior ((convexHull ℝ : (a : Set V) → Set V) s))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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) t))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))

Tactic:
refine this.mono (by gcongr)

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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))
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))))
⊢ Set.Nonempty.{u_1} (α := V) (interior ((convexHull ℝ : (a : Set V) → Set V) s))

Tactic:
suffices (interior (convexHull ℝ (range b))).Nonempty by
    rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
    refine this.mono (by gcongr)
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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))
⊢ t.Finite

Tactic:
b.finite_set

Premises used: AffineBasis.finite_set
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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))
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))))
⊢ 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:
lift t to Finset V using b.finite_set

Premises used: Finset, AffineBasis.finite_set
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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 : 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:
⟨_, b.centroid_mem_interior_convexHull⟩

Premises used: Set.Nonempty, Exists.intro, AffineBasis.centroid_mem_interior_convexHull
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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 : 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:
exact ⟨_, b.centroid_mem_interior_convexHull⟩
-- Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases
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))
rw₁ rw₂ : (interior s).Nonempty ↔ (interior s).Nonempty
⊢ (interior s).Nonempty ↔ Eq (α := AffineSubspace ℝ V) (affineSpan ℝ s) ⊤

Tactic:
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]

Premises used: interior_convexHull_nonempty_iff_affineSpan_eq_top, Convex.convexHull_eq
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
have : ∀ (p : P), asymptoticNhds ℝ P v ≤ cobounded P
⊢ asymptoticNhds ℝ P v ≤ cobounded P

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
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
⊢ asymptoticNhds ℝ P v ≤ cobounded P

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]

Premises used: Filter.map₂_smul, Filter.tendsto_map'_iff, Filter.map_map, Filter.tendsto_id', Filter.vadd_pure, Filter.map_prod_eq_map₂, AffineSpace.asymptoticNhds_eq_smul_vadd, Metric.tendsto_dist_right_atTop_iff
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
change : Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ dist (x.1 • x.2 +ᵥ p) p) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
⊢ 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:
change Tendsto (fun x : ℝ × V => dist (x.1 • x.2 +ᵥ p) p) (atTop ×ˢ 𝓝 v) atTop

Premises used: SProd.sprod, nhds, Prod.fst, HVAdd.hVAdd, Filter.atTop, Filter.Tendsto, HSMul.hSMul, Dist.dist, Prod.snd
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ ‖x.1‖ * ‖x.2‖) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ × V) ↦ dist (x.1 • x.2 +ᵥ p) p) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop

Tactic:
simp_rw [dist_vadd_left, norm_smul]

Premises used: norm_smul, dist_vadd_left
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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) ↦ ‖x.1‖ * ‖x.2‖) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop

Tactic:
Tendsto.atTop_mul_pos (norm_pos_iff.mpr hv)
    (tendsto_norm_atTop_atTop.comp tendsto_id.fst)
    tendsto_snd.norm

Premises used: Iff.mpr, norm_pos_iff, Filter.tendsto_id, Filter.Tendsto.norm, tendsto_norm_atTop_atTop, Filter.Tendsto.atTop_mul_pos, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.Tendsto.fst
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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) ↦ ‖x.1‖ * ‖x.2‖) (SProd.sprod (α := Filter ℝ) atTop (𝓝 v)) atTop

Tactic:
exact Tendsto.atTop_mul_pos (norm_pos_iff.mpr hv)
    (tendsto_norm_atTop_atTop.comp tendsto_id.fst)
    tendsto_snd.norm

Premises used: Iff.mpr, norm_pos_iff, Filter.tendsto_id, Filter.Tendsto.norm, tendsto_norm_atTop_atTop, Filter.Tendsto.atTop_mul_pos, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.Tendsto.fst
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
by_contra! : ∀ (hv : v ∉ {0}), False
⊢ Membership.mem (γ := Set V) {0} v

Tactic:
by_contra! hv
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
hv : v ∉ {0}
⊢ False

Tactic:
h (asymptoticNhds_le_cobounded hv hs)

Premises used: AffineSpace.asymptoticNhds_le_cobounded
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
hv : v ∉ {0}
⊢ False

Tactic:
exact h (asymptoticNhds_le_cobounded hv hs)

Premises used: AffineSpace.asymptoticNhds_le_cobounded
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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

Tactic:
le_antisymm ?_ <| iSup₂_le fun _ h => asymptoticNhds_le_cobounded <|
    Metric.ne_of_mem_sphere h one_ne_zero

Premises used: iSup₂_le, Metric.ne_of_mem_sphere, le_antisymm, AffineSpace.asymptoticNhds_le_cobounded, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
refine : cobounded P ≤ ⨆ (v : V), ⨆ (_ : Membership.mem (γ := Set V) (Metric.sphere 0 1) v), asymptoticNhds ℝ P v
⊢ 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

Premises used: iSup₂_le, Metric.ne_of_mem_sphere, le_antisymm, AffineSpace.asymptoticNhds_le_cobounded, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
have : ∀ (p : P), s ∈ cobounded P
⊢ s ∈ cobounded P

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
⊢ ∀ (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

Premises used: Filter.mem_iSup, Filter.vadd_pure, AffineSpace.asymptoticNhds_eq_smul_vadd
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
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
⊢ s ∈ cobounded P

Tactic:
choose! t ht u hu smul_subset_s using hs
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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
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
⊢ s ∈ cobounded P

Tactic:
have ⟨cover, h₁, h₂⟩ := (isCompact_sphere 0 1).elim_nhds_subcover u hu
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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)
rw : s ∈ comap (dist p) atTop
⊢ s ∈ cobounded P

Tactic:
rw [← Metric.comap_dist_left_atTop p]

Premises used: Metric.comap_dist_left_atTop
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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

Tactic:
⟨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 => ?_⟩

Premises used: Iff.mpr, Set.Ioi, Set.Mem, Set.iInter, Filter.inter_mem, setOf, Filter.Ioi_mem_atTop, Inter.inter, Finset.iInter_mem_sets, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone
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)
refine : ∀ (x : P) (hx : x ∈ dist p ⁻¹' (Set.Ioi 0 ∩ ⋂ x ∈ cover, t x)), x ∈ s
⊢ s ∈ comap (dist p) atTop

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 => ?_⟩