awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
⊢ s ∥ ⊥ ↔ s = ⊥
have refine : ∀ (h : s ∥ ⊥), s = ⊥
Tactic: refine ⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
h : s ∥ ⊥
⊢ s = ⊥
have rcases : ∀ (v : V) (h : ⊥ = map (↑(constVAdd k P v) : P →ᵃ[k] P) s), s = ⊥
Tactic: rcases h with ⟨v, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v) : P →ᵃ[k] P) s
⊢ s = ⊥
have rwa : ∀ (h : map (↑(constVAdd k P v) : P →ᵃ[k] P) s = ⊥), s = ⊥
Tactic: rwa [eq_comm, map_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v) : P →ᵃ[k] P) s
rwa : ∀ (h : map (↑(constVAdd k P v) : P →ᵃ[k] P) s = ⊥), s = ⊥
⊢ s = ⊥
have rwa₁ : ∀ (h : s = ⊥), s = ⊥
Tactic: rwa [eq_comm, map_eq_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
⊢ ⊥ ∥ s ↔ s = ⊥
have rw : s ∥ ⊥ ↔ s = ⊥
Tactic: rw [parallel_comm, parallel_bot_iff_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
rw : s ∥ ⊥ ↔ s = ⊥
⊢ ⊥ ∥ s ↔ s = ⊥
have rw₁ : s = ⊥ ↔ s = ⊥
Tactic: rw [parallel_comm, parallel_bot_iff_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
have refine_1 : ∀ (h : s₁ ∥ s₂), s₁ = ⊥ → s₂ = ⊥
Tactic: refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
refine_1 : ∀ (h : s₁ ∥ s₂), s₁ = ⊥ → s₂ = ⊥
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
have refine_2 : ∀ (h : s₁ ∥ s₂), s₂ = ⊥ → s₁ = ⊥
Tactic: refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
refine_1 : ∀ (h : s₁ ∥ s₂), s₁ = ⊥ → s₂ = ⊥
refine_2 : ∀ (h : s₁ ∥ s₂), s₂ = ⊥ → s₁ = ⊥
⊢ s₁ ∥ s₂ ↔ s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
have refine_3 : ∀ (h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)), s₁ ∥ s₂
Tactic: refine ⟨fun h => ⟨h.direction_eq, ?_, ?_⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂
have hd : s₁.direction = s₂.direction
Tactic: rcases h with ⟨hd, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
hd : s₁.direction = s₂.direction
⊢ s₁ ∥ s₂
have hb : s₁ = ⊥ ↔ s₂ = ⊥
Tactic: rcases h with ⟨hd, hb⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
⊢ s₁ ∥ s₂
have pos : ∀ (hs₁ : s₁ = ⊥), s₁ ∥ s₂
Tactic: by_cases hs₁ : s₁ = ⊥
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
pos : ∀ (hs₁ : s₁ = ⊥), s₁ ∥ s₂
⊢ s₁ ∥ s₂
have neg : ∀ (hs₁ : ¬s₁ = ⊥), s₁ ∥ s₂
Tactic: by_cases hs₁ : s₁ = ⊥
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : s₁ = ⊥
⊢ s₁ ∥ s₂
have pos : s₂ = ⊥
Tactic: rw [hs₁, bot_parallel_iff_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
⊢ s₁ ∥ s₂
have hs₂ : s₂ ≠ ⊥
Tactic: have hs₂ : s₂ ≠ ⊥ := hb.not.1 hs₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
⊢ s₁ ∥ s₂
have neg : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), s₁ ∥ s₂
Tactic: rcases (nonempty_iff_ne_bot s₁).2 hs₁ with ⟨p₁, hp₁⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
⊢ s₁ ∥ s₂
have neg : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), s₁ ∥ s₂
Tactic: rcases (nonempty_iff_ne_bot s₂).2 hs₂ with ⟨p₂, hp₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ s₁ ∥ s₂
have neg : p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁
Tactic: refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
neg : p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁
⊢ s₁ ∥ s₂
have neg₁ : s₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁).direction
Tactic: refine ⟨p₂ -ᵥ p₁, (eq_iff_direction_eq_of_mem hp₂ ?_).2 ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ ∃ y ∈ s₁, ((↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) : (a : P) → P) y = p₂
have neg : ((↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) : (a : P) → P) p₁ = p₂
Tactic: refine ⟨p₁, hp₁, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
h : affineSpan k s₁ ∥ affineSpan k s₂
⊢ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂)
have simp_rw : Eq (α := Submodule k V) (direction (affineSpan k s₁)) (direction (affineSpan k s₂))
Tactic: simp_rw [← direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂) ∧ (s₁ = ∅ ↔ s₂ = ∅)
have rw : affineSpan k s₁ ∥ affineSpan k s₂ ↔
  Eq (α := Submodule k V) (direction (affineSpan k s₁)) (vectorSpan k s₂) ∧
    (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ s₂ = ∅)
Tactic: rw [← direction_affineSpan, ← affineSpan_eq_bot k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔
    Eq (α := Submodule k V) (direction (affineSpan k s₁)) (vectorSpan k s₂) ∧
      (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ s₂ = ∅)
have rw : affineSpan k s₁ ∥ affineSpan k s₂ ↔
  Eq (α := Submodule k V) (direction (affineSpan k s₁)) (direction (affineSpan k s₂)) ∧
    (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ Eq (α := AffineSubspace k P) (affineSpan k s₂) ⊥)
Tactic: rw [← direction_affineSpan, ← affineSpan_eq_bot k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : Set P
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂) ∧ (s₁ = ∅ ↔ s₂ = ∅)
have repeat : affineSpan k s₁ ∥ affineSpan k s₂ ↔
  Eq (α := Submodule k V) (direction (affineSpan k s₁)) (direction (affineSpan k s₂)) ∧
    (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ Eq (α := AffineSubspace k P) (affineSpan k s₂) ⊥)
Tactic: repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : IsDomain k
inst_5 : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
⊢ Parallel (P := P) (affineSpan k {p₁, q₁}) (affineSpan k {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
have rw : Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
  ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
Tactic: rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, vectorSpan_pair_rev,
    vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : IsDomain k
inst_5 : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
rw :
  Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
⊢ Parallel (P := P) (affineSpan k {p₁, q₁}) (affineSpan k {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
have rw₁ : Eq (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
Tactic: rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, vectorSpan_pair_rev,
    vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : IsDomain k
inst_5 : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
rw :
  Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
rw₁ : Eq (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
⊢ Parallel (P := P) (affineSpan k {p₁, q₁}) (affineSpan k {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
have rw₂ : Eq (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (k ∙ (q₂ -ᵥ p₂)) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
Tactic: rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, vectorSpan_pair_rev,
    vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : IsDomain k
inst_5 : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
rw :
  Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
rw₁ : Eq (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
rw₂ : Eq (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (k ∙ (q₂ -ᵥ p₂)) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
⊢ Parallel (P := P) (affineSpan k {p₁, q₁}) (affineSpan k {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
have rw₃ : (∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂) ↔ ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
Tactic: rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, vectorSpan_pair_rev,
    vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : IsDomain k
inst_5 : Module.IsTorsionFree k V
p₁ q₁ p₂ q₂ : P
⊢ Parallel (P := P) (affineSpan k {p₁, q₁}) (affineSpan k {p₂, q₂}) ↔ ∃ (z : kˣ), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw : (∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂) ↔ ∃ (z : kˣ), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [affineSpan_pair_parallel_iff_exists_unit_smul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw : LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
  ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
rw :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw₁ : LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
  ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
rw :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₁ :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw₂ : LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
rw :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₁ :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₂ :
  LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw₃ : LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (k ∙ (q₂ -ᵥ p₂)) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
rw :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₁ :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₂ :
  LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₃ : LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (k ∙ (q₂ -ᵥ p₂)) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw₄ : Membership.mem (γ := Submodule k V) (k ∙ (q₂ -ᵥ p₂)) (q₁ -ᵥ p₁) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ q₁ p₂ q₂ : P
rw :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₁ :
  LE.le (α := Submodule k V) (vectorSpan k (P := P) {p₁, q₁}) (vectorSpan k (P := P) {p₂, q₂}) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₂ :
  LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (vectorSpan k (P := P) {p₂, q₂}) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₃ : LE.le (α := Submodule k V) (k ∙ (q₁ -ᵥ p₁)) (k ∙ (q₂ -ᵥ p₂)) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
rw₄ : Membership.mem (γ := Submodule k V) (k ∙ (q₂ -ᵥ p₂)) (q₁ -ᵥ p₁) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ LE.le (α := Submodule k V) (direction (P := P) (affineSpan k {p₁, q₁})) (direction (P := P) (affineSpan k {p₂, q₂})) ↔
    ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
have rw₅ : (∃ (a : k), a • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁) ↔ ∃ (z : k), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Tactic: rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ : P
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₂}) (affineSpan k {p₂, p₁})
have rw : Eq (α := AffineSubspace k P) (affineSpan k {p₂, p₁}) (affineSpan k {p₂, p₁})
Tactic: rw [Set.pair_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₁
hp₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
hp₁₂ : p₁ ≠ p₂
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₂}) (affineSpan k {p₃, p₄})
have refine : LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
Tactic: refine le_antisymm (affineSpan_pair_le_of_mem_of_mem hp₁ hp₂) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₁
hp₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
hp₁₂ : p₁ ≠ p₂
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have hp₃ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
Tactic: rw [← vsub_vadd p₁ p₃, vadd_left_mem_affineSpan_pair] at hp₁
Cleared hypotheses: hp₁, hp₂, hp₁₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
hp₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
hp₁₂ : p₁ ≠ p₂
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
have rcases : ∀ (r₁ : k) (hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃),
  LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
Tactic: rcases hp₁ with ⟨r₁, hp₁⟩
Cleared hypotheses: hp₁