awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw₂ : dist c₁ c₂ ≤ (dist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₂ : dist c₁ c₂ ≤ (dist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw₃ : dist c₁ c₂ ≤ dist c₁ c₂ * ((dist p₁ p₂)⁻¹ * dist p₁ p₂)
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₂ : dist c₁ c₂ ≤ (dist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₃ : dist c₁ c₂ ≤ dist c₁ c₂ * ((dist p₁ p₂)⁻¹ * dist p₁ p₂)
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw₄ : dist c₁ c₂ ≤ dist c₁ c₂ * 1
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
W : Type u_3
Q : Type u_4
inst : NormedAddCommGroup W
inst_1 : MetricSpace Q
inst_2 : NormedAddTorsor W Q
𝕜 : Type u_5
inst_3 : NormedField 𝕜
inst_4 : NormedSpace 𝕜 W
p₁ p₂ : Q
h : p₁ ≠ p₂
c₁ c₂ : 𝕜
rw : dist c₁ c₂ ≤ (↑(nndist p₁ p₂)⁻¹ : ℝ) * (dist c₁ c₂ * dist p₁ p₂)
rw₁ : dist c₁ c₂ ≤ (↑(nndist p₁ p₂) : ℝ)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₂ : dist c₁ c₂ ≤ (dist p₁ p₂)⁻¹ * (dist c₁ c₂ * dist p₁ p₂)
rw₃ : dist c₁ c₂ ≤ dist c₁ c₂ * ((dist p₁ p₂)⁻¹ * dist p₁ p₂)
rw₄ : dist c₁ c₂ ≤ dist c₁ c₂ * 1
⊢ dist c₁ c₂ ≤
    (↑(nndist p₁ p₂)⁻¹ : ℝ) *
      dist.{u_4} (α := Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₁ : Q) ((lineMap p₁ p₂ : (a : 𝕜) → Q) c₂ : Q)
have rw₅ : dist c₁ c₂ ≤ dist c₁ c₂
Tactic: rw [dist_lineMap_lineMap, NNReal.coe_inv, ← dist_nndist, mul_left_comm,
      inv_mul_cancel₀ (dist_ne_zero.2 h), mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsor (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
P : Type u_3
inst_4 : PseudoMetricSpace P
inst_5 : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
⊢ edist (k • x +ᵥ c) (k • y +ᵥ c) = (↑‖k‖₊ : ENNReal) * edist x y
have rw : edist (k • x) (k • y) = (↑‖k‖₊ : ENNReal) * edist x y
Tactic: rw [show edist (k • x +ᵥ c) (k • y +ᵥ c) = _ from (IsometryEquiv.vaddConst c).isometry ..]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have inl : Subsingleton ι →
  Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
Tactic: cases subsingleton_or_nontrivial ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
inl :
  Subsingleton ι →
    Eq.{u_2 + 1} (α := Set E)
      (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have inr : Nontrivial ι →
  Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
Tactic: cases subsingleton_or_nontrivial ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Subsingleton ι
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have this : Eq.{u_2 + 1} (α := Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) univ
Tactic: have : range b = univ :=
      AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have this : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := b.finiteDimensional
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)
have rw : Eq.{u_2 + 1} (α := Set E) (⋂ (i : ι), {x : E | LE.le (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)})
  (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0))
Tactic: rw [b.convexHull_eq_nonneg_coord, setOf_forall]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have this₁ : Eq.{u_2 + 1} (α := Set E)
  ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
  (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)
Tactic: have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
      rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : Finite ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h : Nontrivial ι
this_1 : FiniteDimensional ℝ E
this :
  Eq.{u_2 + 1} (α := Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    (⋂ (i : ι), preimage (β := ℝ) (⇑(b.coord i) : (a : E) → ℝ) (Ici 0) : Set E)
⊢ Eq.{u_2 + 1} (α := Set E)
    (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)}
have inr : ∀ (x : E),
  Membership.mem (γ := Set E)
      (interior ((convexHull ℝ : (a : Set E) → Set E) (range.{u_2, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((b.coord i : (a : E) → ℝ) x : ℝ)} x
Tactic: ext
-- 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
hne : s.Nonempty
h : AffineIndependent.{0, u_1, u_2, u_2} ℝ (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ ∃ (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 obtain : ∀ (q : P) (hq : q ∈ s),
  ∃ (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: obtain ⟨q, hq⟩ := hne
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
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
⊢ ∃ (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 obtain : ∀ (ε : ℝ) (ε0 : 0 < ε) (hεu : Metric.closedBall q ε ⊆ 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) ⊤
Tactic: obtain ⟨ε, ε0, hεu⟩ := Metric.nhds_basis_closedBall.mem_iff.1 (hu.mem_nhds <| hsu hq)
-- 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),
    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 obtain : ∀ (t : Set P) (ht₁ : s ⊆ t) (ht₂ : AffineIndependent ℝ (P := P) fun (p : (↑t : Type u_2)) ↦ (↑p : P))
  (ht₃ : 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) ⊤
Tactic: obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affineIndependent_affineSpan_eq_top h
-- 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)
⊢ ∀ (y : P), f y ∈ u
have refine : ∀ (y : P), f y ∈ Metric.closedBall q ε
Tactic: refine fun y => hεu ?_
-- 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)
y : P
⊢ Membership.mem (α := P) (Metric.closedBall q ε) ((lineMap q y : (a : ℝ) → P) (ε / dist y q) : P)
have rw : ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (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
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)
⊢ ∃ (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 hf : ∀ (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 _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.AddTorsorBases (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
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
⊢ ∃ (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 hεyq : ∀ 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)
-- 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) ⋯
⊢ ∃ (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 : s ⊆ range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)
Tactic: refine ⟨Set.range fun p : t => lineMap q p (w 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_1 : 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 : (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) ⊆ u
Tactic: refine ⟨Set.range fun p : t => lineMap q p (w 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_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
⊢ ∃ (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 : 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: refine ⟨Set.range fun p : t => lineMap q p (w 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_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))
⊢ ∃ (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 : Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
  (affineSpan ℝ (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ))) ⊤
Tactic: refine ⟨Set.range fun p : t => lineMap q p (w 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 ∈ s
⊢ Membership.mem (γ := Set P) (range fun (p : (↑t : Type u_2)) ↦ (lineMap q (↑p : P) : (a : ℝ) → P) (↑(w p) : ℝ)) p
have 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 sorry) =
  p
Tactic: use ⟨p, ht₁ hp⟩