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
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
⊢ (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
have 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
Tactic: by_cases hps : p ∈ s
-- 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
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
⊢ (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
have 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
Tactic: by_cases hps : p ∈ s
-- 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
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
⊢ (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
have pos : p ∈ u
Tactic: simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]
-- 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
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
⊢ (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
have neg : Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)
Tactic: simp only [w, hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff,
      Units.val_one]
-- 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
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
⊢ (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
have 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
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]
-- 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
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
⊢ (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
have 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
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]
-- 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
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
⊢ (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
have pos₄ : ∀ (hps : p ∈ s), p ∈ 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]
-- 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
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
⊢ (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
have neg₄ : ∀ (hps : p ∉ s), Membership.mem (α := P) u ((lineMap q p : (a : ℝ) → P) (ε / dist p q) : P)
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]
-- 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
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) ⊤
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
have refine_4₁ : Eq.{u_2 + 1} (α := AffineSubspace ℝ P) ⊤ ⊤
Tactic: rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]
-- 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
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) ⊤
⊢ ∃ (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) ⊤
have 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) sorry;
s ⊆ range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)
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₃]
-- 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
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) : ℝ)
⊢ ∃ (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) ⊤
have 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) sorry;
(range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) ⊆ u
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₃]
-- 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
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
⊢ ∃ (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) ⊤
have 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) sorry;
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: 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₃]
-- 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
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))
⊢ ∃ (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) ⊤
have 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) sorry;
Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
  (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
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₃]