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
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)
y : P
⊢ ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε

Tactic:
exact mul_le_of_le_one_left ε0.le (div_self_le_one _)

Premises used: LT.lt.le, div_self_le_one, mul_le_of_le_one_left
-- 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)
⊢ ∀ (y : P), f y ∈ u

Tactic:
have hf : ∀ y, f y ∈ u := by
    refine fun y => hεu ?_
    simp only [f]
    rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs,
      dist_eq_norm_vsub V y q, abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]
    exact mul_le_of_le_one_left ε0.le (div_self_le_one _)
-- 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
⊢ ∀ y ∉ s, ε / dist y q ≠ 0

Tactic:
have hεyq : ∀ y ∉ s, ε / dist y q ≠ 0 := fun y hy =>
    div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm)
-- 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
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) ⋯
⊢ ∃ (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:
⟨Set.range fun p : t => lineMap q p (w p : ℝ), ?_, ?_, ?_, ?_⟩

Premises used: Units.val, AffineMap.lineMap, And.intro, Exists.intro, Set.range, Subtype.val, DFunLike.coe
-- 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
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) ⋯
refine_1 : s ⊆ range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)
refine_2 : (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) ⊆ u
refine_3 :
  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 :
  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:
refine ⟨Set.range fun p : t => lineMap q p (w p : ℝ), ?_, ?_, ?_, ?_⟩
-- 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
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) ⋯
p : P
hp : p ∈ s
h₁ :
  (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p ⋯) =
    p
⊢ Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) p

Tactic:
use ⟨p, ht₁ hp⟩
-- 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
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) ⋯
p : P
hp : p ∈ s
⊢ (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p ⋯) =
    p

Tactic:
simp [w, hp]
-- 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
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) ⋯
p : P
hp : p ∈ t
pos :
  ∀ (hps : p ∈ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
neg :
  ∀ (hps : p ∉ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
⊢ (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
    u

Tactic:
by_cases hps : p ∈ s
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∈ s
pos : p ∈ u
⊢ (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
    u

Tactic:
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]

Premises used: dif_pos, dif_neg, AffineMap.lineMap_apply_one, Units.val_one, Units.val_mk0, not_false_iff
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∉ s
neg : Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)
⊢ (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
    u

Tactic:
simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]

Premises used: dif_pos, dif_neg, AffineMap.lineMap_apply_one, Units.val_one, Units.val_mk0, not_false_iff
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∈ s
⊢ p ∈ u

Tactic:
hsu hps
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∈ s
⊢ p ∈ u

Tactic:
exact hsu hps
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∉ s
⊢ Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)

Tactic:
hf p

Premises used: Set.Mem
-- 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
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) ⋯
p : P
hp : p ∈ t
hps : p ∉ s
⊢ Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)

Tactic:
exact hf p
-- 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
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) ⋯
p : P
hp : p ∈ t
pos :
  ∀ (hps : p ∈ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
neg :
  ∀ (hps : p ∉ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
pos₁ :
  ∀ (hps : p ∈ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
neg₁ :
  ∀ (hps : p ∉ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
pos₂ :
  ∀ (hps : p ∈ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
neg₂ :
  ∀ (hps : p ∉ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
pos₃ :
  ∀ (hps : p ∈ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
neg₃ :
  ∀ (hps : p ∉ s),
    (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
        (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
      u
pos₄ : ∀ (hps : p ∈ s), p ∈ u
neg₄ : ∀ (hps : p ∉ s), Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)
pos₅ : ∀ (hps : p ∈ s), p ∈ u
neg₅ : ∀ (hps : p ∉ s), Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)
⊢ (fun (p : (↑t : Type u_2)) ↦ ((lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ) : P))
      (Subtype.mk (p := fun (x : P) ↦ x ∈ t) p hp) ∈
    u

Tactic:
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]

Premises used: dif_pos, dif_neg, AffineMap.lineMap_apply_one, Units.val_one, Units.val_mk0, not_false_iff
-- 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
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))

Tactic:
(ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range

Premises used: Set.Mem, Subtype.mk, AffineIndependent.range, AffineIndependent.units_lineMap
-- 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
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))

Tactic:
exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range

Premises used: Subtype.mk, AffineIndependent.range, AffineIndependent.units_lineMap
-- 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
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) ⋯
refine_4 : Eq (α := AffineSubspace ℝ P) (affineSpan ℝ t) ⊤
refine_4₁ refine_4₂ : Eq.{u_2 + 1} (α := AffineSubspace ℝ P) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤

Tactic:
rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]

Premises used: affineSpan_eq_affineSpan_lineMap_units
-- 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
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) ⊤
⊢ ∃ 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⟩
-- 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
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) ⊤
⊢ ∃ 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⟩

Premises used: Iff.mpr, Set.singleton_nonempty, Set.singleton_subset_iff, IsOpen.exists_between_affineIndependent_span_eq_top, affineIndependent_of_subsingleton