awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂

Tactic:
⟨p₁, hp₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 : ((↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) : (a : P) → P) p₁ = p₂
⊢ ∃ y ∈ s₁, ((↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) : (a : P) → P) y = p₂

Tactic:
refine ⟨p₁, hp₁, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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)
⊢ ((↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) : (a : P) → P) p₁ = p₂

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁)) : P →ᵃ[k] P) s₁).direction

Tactic:
simpa using hd.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
simp_rw : Eq (α := Submodule k V) (direction (affineSpan k s₁)) (direction (affineSpan k s₂))
⊢ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂)

Tactic:
simp_rw [← direction_affineSpan]

Premises used: direction_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) (direction (affineSpan k s₁)) (direction (affineSpan k s₂))

Tactic:
h.direction_eq

Premises used: AffineSubspace.Parallel.direction_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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) (direction (affineSpan k s₁)) (direction (affineSpan k s₂))

Tactic:
exact h.direction_eq

Premises used: AffineSubspace.Parallel.direction_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
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₂ = ∅)
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂) ∧ (s₁ = ∅ ↔ s₂ = ∅)

Tactic:
rw [← direction_affineSpan, ← affineSpan_eq_bot k]

Premises used: direction_affineSpan, affineSpan_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
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₂) ⊥)
⊢ 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]

Premises used: direction_affineSpan, affineSpan_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
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₂) ⊥)
⊢ affineSpan k s₁ ∥ affineSpan k s₂ ↔ Eq (α := Submodule k V) (vectorSpan k s₁) (vectorSpan k s₂) ∧ (s₁ = ∅ ↔ s₂ = ∅)

Tactic:
repeat rw [← direction_affineSpan, ← affineSpan_eq_bot k]

Premises used: direction_affineSpan, affineSpan_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁)) (direction (affineSpan k s₂)) ∧
      (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ Eq (α := AffineSubspace k P) (affineSpan k s₂) ⊥)

Tactic:
parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

Premises used: AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁)) (direction (affineSpan k s₂)) ∧
      (Eq (α := AffineSubspace k P) (affineSpan k s₁) ⊥ ↔ Eq (α := AffineSubspace k P) (affineSpan k s₂) ⊥)

Tactic:
exact parallel_iff_direction_eq_and_eq_bot_iff_eq_bot

Premises used: AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₃ p₄ : P
⊢ Parallel (P := P) (affineSpan k {p₁, p₂}) (affineSpan k {p₃, p₄}) ↔
    Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (vectorSpan k (P := P) {p₃, p₄})

Tactic:
simp [affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, ←
    not_nonempty_iff_eq_empty]

Premises used: AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
rw₃ rw₄ : (∃ (z : kˣ), z • (q₁ -ᵥ p₁) = 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₂

Tactic:
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq, vectorSpan_pair_rev,
    vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton]

Premises used: vectorSpan_pair_rev, Submodule.span_singleton_eq_span_singleton, AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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 : (∃ (z : kˣ), z • (q₁ -ᵥ p₁) = 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₁

Tactic:
rw [affineSpan_pair_parallel_iff_exists_unit_smul']

Premises used: AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
z : kˣ
hz : z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂
⊢ z⁻¹ • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁

Tactic:
simp [← hz]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
h : ∃ (z : kˣ), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
z : kˣ
hz : z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
⊢ z⁻¹ • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂

Tactic:
simp [← hz]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
⊢ (∃ (z : kˣ), z • (q₁ -ᵥ p₁) = q₂ -ᵥ p₂) ↔ ∃ (z : kˣ), z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁

Tactic:
exact ⟨fun ⟨z, hz⟩ ↦ ⟨z⁻¹, by simp [← hz]⟩, fun ⟨z, hz⟩ ↦ ⟨z⁻¹, by simp [← hz]⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁
rw₅ rw₆ : (∃ (a : k), a • (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₁

Tactic:
rw [direction_affineSpan, direction_affineSpan, vectorSpan_pair_rev, vectorSpan_pair_rev,
    Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]

Premises used: direction_affineSpan, Submodule.mem_span_singleton, vectorSpan_pair_rev, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
rw rw₁ : Eq (α := AffineSubspace k P) (affineSpan k {p₂, p₁}) (affineSpan k {p₂, p₁})
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₂}) (affineSpan k {p₂, p₁})

Tactic:
rw [Set.pair_comm]

Premises used: Set.pair_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₄})

Tactic:
le_antisymm (affineSpan_pair_le_of_mem_of_mem hp₁ hp₂) ?_

Premises used: affineSpan_pair_le_of_mem_of_mem, le_antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
refine : LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
⊢ Eq (α := AffineSubspace k P) (affineSpan k {p₁, p₂}) (affineSpan k {p₃, p₄})

Tactic:
refine le_antisymm (affineSpan_pair_le_of_mem_of_mem hp₁ hp₂) ?_

Premises used: affineSpan_pair_le_of_mem_of_mem, le_antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
⊢ ∃ (r : k), r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃

Tactic:
rw [← vsub_vadd p₁ p₃, vadd_left_mem_affineSpan_pair] at hp₁

Premises used: vsub_vadd, vadd_left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
hp₃ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂

Tactic:
rw [← vsub_vadd p₁ p₃, vadd_left_mem_affineSpan_pair] at hp₁

Premises used: vsub_vadd, vadd_left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
hp₃ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
hp₄ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₃, p₄}) p₂
⊢ p₁ ≠ p₂

Tactic:
rw [← vsub_vadd p₁ p₃, vadd_left_mem_affineSpan_pair] at hp₁

Premises used: vsub_vadd, vadd_left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₂
rcases :
  ∀ (r₁ : k) (hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃),
    LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})

Tactic:
rcases hp₁ with ⟨r₁, hp₁⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
rw :
  ∀ (hp₂ : ∃ (r : k), r • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃) (hp₁₂ : p₁ ≠ p₂) (r₁ : k) (hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃),
    LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})

Tactic:
rw [← vsub_vadd p₂ p₃, vadd_left_mem_affineSpan_pair] at hp₂

Premises used: vsub_vadd, vadd_left_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
rcases :
  ∀ (r₂ : k) (hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃),
    LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})

Tactic:
rcases hp₂ with ⟨r₂, hp₂⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
rw : r₂ ≠ r₁
⊢ r₂ - r₁ ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hp₁ : r₂ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
⊢ False

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
⊢ r₂ - r₁ ≠ 0

Tactic:
have hr₀ : r₂ - r₁ ≠ 0 := by
    rw [sub_ne_zero]
    rintro rfl
    simp_all
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
⊢ (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁

Tactic:
simp [sub_smul, hp₁, hp₂]

Premises used: sub_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
⊢ (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁

Tactic:
have hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁ := by
    simp [sub_smul, hp₁, hp₂]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁
⊢ p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)

Tactic:
rw [← eq_inv_smul_iff₀ hr₀] at hr

Premises used: eq_inv_smul_iff₀
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})

Tactic:
affineSpan_pair_le_of_mem_of_mem ?_ ?_

Premises used: affineSpan_pair_le_of_mem_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
refine_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃
refine_2 : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₄
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {p₃, p₄}) (affineSpan k {p₁, p₂})

Tactic:
refine affineSpan_pair_le_of_mem_of_mem ?_ ?_

Premises used: affineSpan_pair_le_of_mem_of_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) ((-r₁ * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁)

Tactic:
smul_vsub_vadd_mem_affineSpan_pair (-r₁ * (r₂ - r₁)⁻¹) p₁ p₂

Premises used: HMul.hMul, HSub.hSub, smul_vsub_vadd_mem_affineSpan_pair, Inv.inv, Neg.neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
h : p₃ = (-r₁ * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₃

Tactic:
convert! smul_vsub_vadd_mem_affineSpan_pair (-r₁ * (r₂ - r₁)⁻¹) p₁ p₂

Premises used: HMul.hMul, HSub.hSub, smul_vsub_vadd_mem_affineSpan_pair, Inv.inv, Neg.neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₃ = (-r₁ * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
simp [mul_smul, ← hr, hp₁]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁)

Tactic:
smul_vsub_vadd_mem_affineSpan_pair ((1 - r₁) * (r₂ - r₁)⁻¹) p₁ p₂

Premises used: HMul.hMul, HSub.hSub, smul_vsub_vadd_mem_affineSpan_pair, Inv.inv, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
h : p₄ = ((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p₄

Tactic:
convert! smul_vsub_vadd_mem_affineSpan_pair ((1 - r₁) * (r₂ - r₁)⁻¹) p₁ p₂

Premises used: HMul.hMul, HSub.hSub, smul_vsub_vadd_mem_affineSpan_pair, Inv.inv, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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₁₂ : p₁ ≠ p₂
r₁ : k
hp₁ : r₁ • (p₄ -ᵥ p₃) = p₁ -ᵥ p₃
r₂ : k
hp₂ : r₂ • (p₄ -ᵥ p₃) = p₂ -ᵥ p₃
hr₀ : r₂ - r₁ ≠ 0
hr : p₄ -ᵥ p₃ = (r₂ - r₁)⁻¹ • (p₂ -ᵥ p₁)
⊢ p₄ = ((1 - r₁) * (r₂ - r₁)⁻¹) • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
simp [mul_smul, ← hr, sub_smul, hp₁]

Premises used: sub_smul, SemigroupAction.mul_smul