-- 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
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P)
ht₃ : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
f : P → P := fun (y : P) ↦ (lineMap q y : (a : ℝ) → P) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
let let₁ let₂ :
  ∃ (t : Set P),
    s ⊆ t ∧
      t ⊆ u ∧
        AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
            (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
          Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
refine_1 :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  s ⊆ range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)
refine_2 :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) ⊆ u
refine_3 :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι :=
    { x : P //
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x })
    (Subtype.val (p := fun (x : P) ↦
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x))
refine_4 :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
refine_2₁ :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) ⊆ u
refine_3₁ :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι :=
    { x : P //
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x })
    (Subtype.val (p := fun (x : P) ↦
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x))
refine_4₁ :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
refine_3₂ :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι :=
    { x : P //
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x })
    (Subtype.val (p := fun (x : P) ↦
      Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))
        x))
refine_4₂ refine_4₃ :
  let w : (↑t : Type u_2) → ℝˣ := fun (p : (↑t : Type u_2)) ↦
    if hp : (↑p : P) ∈ s then 1 else Units.mk0 (ε / dist (↑p : P) q) ⋯;
  Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
⊢ ∃ (t : Set P),
    s ⊆ t ∧
      t ⊆ u ∧
        AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ t })
            (Subtype.val (p := fun (x : P) ↦ x ∈ t)) ∧
          Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤

Tactic:
classical
  let w : t → ℝˣ := fun p => if hp : (p : P) ∈ s then 1 else Units.mk0 _ (hεyq (↑p) hp)
  refine ⟨Set.range fun p : t => lineMap q p (w p : ℝ), ?_, ?_, ?_, ?_⟩
  · intro p hp; use ⟨p, ht₁ hp⟩; simp [w, hp]
  · rintro y ⟨⟨p, hp⟩, rfl⟩
    by_cases hps : p ∈ s <;>
    simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one] <;>
    [exact hsu hps; exact hf p]
  · exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range
  · rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]

Premises used: dif_pos, dif_neg, AffineMap.lineMap_apply_one, Units.val_one, Units.val_mk0, not_false_iff, rfl