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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {p₁, p₂})) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
rw₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
rw₂ rw₃ : (∃ (r : k), r • (p₁ -ᵥ p₂) = v) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₂) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v

Tactic:
rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair]

Premises used: direction_affineSpan, right_mem_affineSpan_pair, mem_vectorSpan_pair, AffineSubspace.vadd_mem_iff_mem_direction
-- 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
mp :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p →
    ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
mpr :
  (∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p) →
    Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p ↔
    ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p

Tactic:
constructor
-- 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
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p
⊢ ∃ (r : k), r • (p₂ -ᵥ p₁) = p -ᵥ p₁

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

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 : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p p₁ p₂ : P
h : ∃ (r : k), r • (p₂ -ᵥ p₁) = p -ᵥ p₁
mp : ∀ (r : k) (hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁), ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p

Tactic:
obtain ⟨r, hr⟩ := h
-- 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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p

Tactic:
⟨r, ?_⟩

Premises used: 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
p p₁ p₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
mp : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p

Tactic:
refine ⟨r, ?_⟩
-- 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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
mp : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = (p -ᵥ p₁) +ᵥ p₁
mp₁ : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = r • (p₂ -ᵥ p₁) +ᵥ p₁
mp₂ mp₃ : r • (p₂ -ᵥ p₁) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p

Tactic:
rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply, vsub_vadd
-- 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
r : k
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k {p₁, p₂})
    ((AffineMap.lineMap p₁ p₂ : (a : k) → P) r : P)

Tactic:
AffineMap.lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_mem_affineSpan_pair
-- 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
r : k
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k {p₁, p₂})
    ((AffineMap.lineMap p₁ p₂ : (a : k) → P) r : P)

Tactic:
exact AffineMap.lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_mem_affineSpan_pair
-- 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
rw :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₁}) p ↔
    ∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p
rw₁ rw₂ :
  (∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p) ↔ ∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p ↔
    ∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p

Tactic:
rw [Set.pair_comm, mem_affineSpan_pair_iff_exists_lineMap_eq]

Premises used: mem_affineSpan_pair_iff_exists_lineMap_eq, Set.pair_comm
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
refine_1 : (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
refine_2 : s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ p₁ ∈ (↑s₁ : Set P)

Tactic:
rw [← mem_coe] at hp₁

Premises used: AffineSubspace.mem_coe
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
hp₃ : p₁ ∈ (↑s₁ : Set P)
⊢ p₂ ∈ s₂

Tactic:
rw [← mem_coe] at hp₁

Premises used: AffineSubspace.mem_coe
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
refine_1 :
  (fun (x : P) ↦ x -ᵥ p₁) '' ((↑s₁ : Set P) ∪ (↑s₂ : Set P)) ⊆ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
⊢ direction (affineSpan k ((↑s₁ : Set P) ∪ (↑s₂ : Set P))) ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp₁),
      Submodule.span_le]

Premises used: direction_affineSpan, Set.mem_union_left, vectorSpan_eq_span_vsub_set_right, Submodule.span_le
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P) ∪ (↑s₂ : Set P)
refine_1 :
  ∀ (hp₃ : p₃ ∈ (↑s₁ : Set P)), (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
refine_1₁ :
  ∀ (hp₃ : p₃ ∈ (↑s₂ : Set P)), (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)

Tactic:
rcases hp₃ with hp₃ | 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P)
refine_1 : ∃ y ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s₁.direction, y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)

Tactic:
rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]

Premises used: sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P)
right : 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
⊢ ∃ y ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s₁.direction, y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃

Tactic:
use 0, Submodule.zero_mem _, p₃ -ᵥ p₁, vsub_mem_direction hp₃ hp₁

Premises used: AffineSubspace.vsub_mem_direction, Submodule.zero_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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P)
right right₁ : p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃
⊢ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
refine_1 : ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)

Tactic:
rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]

Premises used: sup_assoc, SetLike.mem_coe, Submodule.mem_sup
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
h : p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
⊢ ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃

Tactic:
use 0, Submodule.zero_mem _, p₃ -ᵥ p₁

Premises used: Submodule.zero_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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
h : p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃

Tactic:
rw [and_comm, zero_add]

Premises used: and_comm, zero_add
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
right : p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
use rfl

Premises used: rfl
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
right :
  ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
rw [← vsub_add_vsub_cancel p₃ p₂ p₁, Submodule.mem_sup]

Premises used: vsub_add_vsub_cancel, Submodule.mem_sup
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
w : V
left : p₃ -ᵥ p₂ ∈ s₂.direction
w₁ : V
left₁ : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (p₂ -ᵥ p₁)
right : p₃ -ᵥ p₂ + (p₂ -ᵥ p₁) = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
⊢ ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)

Tactic:
use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _

Premises used: AffineSubspace.vsub_mem_direction, Submodule.mem_span_singleton_self
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
sup_le (sup_direction_le _ _) ?_

Premises used: AffineSubspace.sup_direction_le, sup_le
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
refine_2 : k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
refine sup_le (sup_direction_le _ _) ?_

Premises used: AffineSubspace.sup_direction_le, sup_le
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ LE.le (α := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (Submodule.span k ((↑(s₁ ⊔ s₂) : Set P) -ᵥ (↑(s₁ ⊔ s₂) : Set P)))

Tactic:
sInf_le_sInf fun p hp =>
        Set.Subset.trans
          (Set.singleton_subset_iff.2
            (vsub_mem_vsub (mem_affineSpan k (Set.mem_union_right _ hp₂))
              (mem_affineSpan k (Set.mem_union_left _ hp₁))))
          hp

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, Set.Subset.trans, sInf_le_sInf, Set.mem_union_right, mem_affineSpan, SetLike.coe, Set.vsub_mem_vsub, Set.mem_union_left
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ LE.le (α := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (Submodule.span k ((↑(s₁ ⊔ s₂) : Set P) -ᵥ (↑(s₁ ⊔ s₂) : Set P)))

Tactic:
exact
      sInf_le_sInf fun p hp =>
        Set.Subset.trans
          (Set.singleton_subset_iff.2
            (vsub_mem_vsub (mem_affineSpan k (Set.mem_union_right _ hp₂))
              (mem_affineSpan k (Set.mem_union_left _ hp₁))))
          hp

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Subset.trans, sInf_le_sInf, Set.mem_union_right, mem_affineSpan, Set.vsub_mem_vsub, Set.mem_union_left
-- 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
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
rw : s₁.direction ⊔ s₂.direction ⊔ k ∙ (p -ᵥ p) = s₁.direction ⊔ s₂.direction
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction

Tactic:
rw [direction_sup hp₁ hp₂]

Premises used: AffineSubspace.direction_sup
-- 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
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p -ᵥ p) = s₁.direction ⊔ s₂.direction

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 : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
rw : direction (affineSpan k ((↑s : Set P) ∪ (↑(affineSpan k {p₂}) : Set P))) = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
⊢ direction (affineSpan k (insert p₂ (↑s : Set P))) = k ∙ (p₂ -ᵥ p₁) ⊔ s.direction

Tactic:
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]

Premises used: sup_comm, Set.union_singleton, AffineSubspace.coe_affineSpan_singleton
-- 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 : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
rw : s.direction ⊔ vectorSpan k (P := P) {p₂} ⊔ k ∙ (p₂ -ᵥ p₁) = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
⊢ (s ⊔ affineSpan k {p₂}).direction = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
rw [direction_sup hp₁ (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]

Premises used: Set.mem_singleton, direction_affineSpan, mem_affineSpan, AffineSubspace.direction_sup
-- 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 : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ s.direction ⊔ vectorSpan k (P := P) {p₂} ⊔ k ∙ (p₂ -ᵥ p₁) = s.direction ⊔ k ∙ (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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ s
p₂ p : P
rw :
  ∀ (hp₁ : p₁ ∈ (↑s : Set P)) (p₂ p : P),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (insert p₂ (↑s : Set P))) p ↔
      ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (insert p₂ (↑s : Set P))) p ↔
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [← mem_coe] at hp₁

Premises used: AffineSubspace.mem_coe
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
rw :
  (∃ (y : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = p -ᵥ p₁) ↔
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (insert p₂ (↑s : Set P))) p ↔
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),
    direction_affineSpan_insert hp₁, Submodule.mem_sup]

Premises used: AffineSubspace.direction_affineSpan_insert, Set.mem_insert_of_mem, mem_affineSpan, Submodule.mem_sup, AffineSubspace.vsub_right_mem_direction_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
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
mp :
  (∃ (y : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = p -ᵥ p₁) →
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
mpr :
  (∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0) →
    ∃ (y : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = p -ᵥ p₁
⊢ (∃ (y : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) y ∧ ∃ z ∈ s.direction, y + z = p -ᵥ p₁) ↔
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
constructor
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₁ : V
hv₁ : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) v₁
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
mp :
  ∀ (hv₁ : ∃ (a : k), a • (p₂ -ᵥ p₁) = v₁) (v₂ : V) (hv₂ : v₂ ∈ s.direction) (hp : v₁ + v₂ = p -ᵥ p₁),
    ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [Submodule.mem_span_singleton] at hv₁

Premises used: Submodule.mem_span_singleton
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₁ : V
hv₁ : ∃ (a : k), a • (p₂ -ᵥ p₁) = v₁
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
mp : ∀ (r : k) (hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁), ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rcases hv₁ with ⟨r, rfl⟩

Premises used: rfl
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
right : p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂

Tactic:
symm at 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
⊢ p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁

Tactic:
rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp

Premises used: sub_eq_zero, vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
right : (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
right₁ right₂ : (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁ = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
rw [hp, vadd_vadd]

Premises used: vadd_vadd