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
p₁ p₂ : P
v : V
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₂) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
have rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {p₁, p₂})) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair]
-- 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
v : V
rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {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
have rw₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair]
-- 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
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
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₂) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
have rw₂ : (∃ (r : k), r • (p₁ -ᵥ p₂) = v) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair]
-- 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₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p ↔
    ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p →
  ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
Tactic: constructor
-- 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₂ : P
mp :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) 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
have mpr : (∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p) →
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p
Tactic: constructor
-- 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
p p₁ p₂ : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have h₁ : ∃ (r : k), r • (p₂ -ᵥ p₁) = p -ᵥ p₁
Tactic: rw [← vsub_vadd p p₁, vadd_left_mem_affineSpan_pair] 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
p p₁ p₂ : P
h : ∃ (r : k), r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp : ∀ (r : k) (hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁), ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
Tactic: obtain ⟨r, hr⟩ := 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
p p₁ p₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ (r : k), (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
Tactic: refine ⟨r, ?_⟩
-- 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₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = (p -ᵥ p₁) +ᵥ p₁
Tactic: rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]
-- 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₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
mp : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = (p -ᵥ p₁) +ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp₁ : (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = r • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]
-- 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₂ : 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₁
⊢ (AffineMap.lineMap p₁ p₂ : (a : k) → P) r = p
have mp₂ : r • (p₂ -ᵥ p₁) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ p₁
Tactic: rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]
-- 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₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) p ↔
    ∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p
have rw : 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]
-- 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₂ : P
rw :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₂, p₁}) 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
have rw₁ : (∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p) ↔ ∃ (r : k), (AffineMap.lineMap p₂ p₁ : (a : k) → P) r = p
Tactic: rw [Set.pair_comm, mem_affineSpan_pair_iff_exists_lineMap_eq]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have refine_1 : (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Tactic: refine le_antisymm ?_ ?_
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
refine_1 : (s₁ ⊔ s₂).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have refine_2 : s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
Tactic: refine le_antisymm ?_ ?_
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ direction (affineSpan k ((↑s₁ : Set P) ∪ (↑s₂ : Set P))) ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have hp₃ : p₁ ∈ (↑s₁ : Set P)
Tactic: rw [← mem_coe] at hp₁
Cleared hypotheses: 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 : 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₂
⊢ direction (affineSpan k ((↑s₁ : Set P) ∪ (↑s₂ : Set P))) ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have refine_1 : (fun (x : P) ↦ x -ᵥ p₁) '' ((↑s₁ : Set P) ∪ (↑s₂ : Set P)) ⊆ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
Tactic: rw [direction_affineSpan, vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ hp₁),
      Submodule.span_le]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P) ∪ (↑s₂ : Set P)
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
have refine_1 : ∀ (hp₃ : p₃ ∈ (↑s₁ : Set P)), (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
Tactic: rcases hp₃ with hp₃ | hp₃
Cleared hypotheses: 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
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)
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
have refine_1₁ : ∀ (hp₃ : p₃ ∈ (↑s₂ : Set P)), (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
Tactic: rcases hp₃ with hp₃ | hp₃
Cleared hypotheses: 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P)
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
have refine_1 : ∃ y ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s₁.direction, y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
Tactic: rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₁ : Set P)
⊢ ∃ y ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s₁.direction, y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
have right : 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
Tactic: use 0, Submodule.zero_mem _, p₃ -ᵥ p₁, vsub_mem_direction 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 : 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)
⊢ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
have right : p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃
Tactic: rw [zero_add]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ (fun (x : P) ↦ x -ᵥ p₁) p₃ ∈ (↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)) : Set V)
have refine_1 : ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
Tactic: rw [sup_assoc, SetLike.mem_coe, Submodule.mem_sup]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), y + z = (fun (x : P) ↦ x -ᵥ p₁) p₃
have h : p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
Tactic: use 0, Submodule.zero_mem _, p₃ -ᵥ p₁
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun (x : P) ↦ x -ᵥ p₁) p₃
have h : p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Tactic: rw [and_comm, zero_add]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ p₃ -ᵥ p₁ = (fun (x : P) ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have right : p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Tactic: use rfl
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have right : ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
Tactic: rw [← vsub_add_vsub_cancel p₃ p₂ p₁, Submodule.mem_sup]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
⊢ ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
have w : V
Tactic: use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ (↑s₂ : Set P)
w : V
⊢ ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
have left : p₃ -ᵥ p₂ ∈ s₂.direction
Tactic: use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _
-- 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
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
⊢ ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
have left₁ : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (p₂ -ᵥ p₁)
Tactic: use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _
-- 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
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₁)
⊢ ∃ y ∈ s₂.direction, ∃ (z : V), Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) z ∧ y + z = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
have right : p₃ -ᵥ p₂ + (p₂ -ᵥ p₁) = p₃ -ᵥ p₂ + (p₂ -ᵥ p₁)
Tactic: use p₃ -ᵥ p₂, vsub_mem_direction hp₃ hp₂, p₂ -ᵥ p₁, Submodule.mem_span_singleton_self _
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
have refine_2 : k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction
Tactic: refine sup_le (sup_direction_le _ _) ?_
-- 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
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction
have rw : s₁.direction ⊔ s₂.direction ⊔ k ∙ (p -ᵥ p) = s₁.direction ⊔ s₂.direction
Tactic: rw [direction_sup 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 : 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
⊢ direction (affineSpan k (insert p₂ (↑s : Set P))) = k ∙ (p₂ -ᵥ p₁) ⊔ s.direction
have rw : direction (affineSpan k ((↑s : Set P) ∪ (↑(affineSpan k {p₂}) : Set P))) = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Tactic: rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]
-- 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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (s ⊔ affineSpan k {p₂}).direction = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
have rw : s.direction ⊔ vectorSpan k (P := P) {p₂} ⊔ k ∙ (p₂ -ᵥ p₁) = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Tactic: rw [direction_sup hp₁ (mem_affineSpan k (Set.mem_singleton _)), 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ s
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
have 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
Tactic: rw [← mem_coe] at hp₁
Cleared hypotheses: hp₁, p₂, p
-- 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
p₁ : P
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
have 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
Tactic: rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),
    direction_affineSpan_insert hp₁, Submodule.mem_sup]
-- 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
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
p₂ 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
have 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
Tactic: constructor
-- 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
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
⊢ (∃ (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
have 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₁
Tactic: constructor
-- 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
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₁
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
have 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
Tactic: rw [Submodule.mem_span_singleton] at hv₁
Cleared hypotheses: hv₁, v₂, hv₂, 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 : 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₁
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
have mp : ∀ (r : k) (hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁), ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
Tactic: rcases hv₁ with ⟨r, rfl⟩
Cleared hypotheses: v₁, hv₁, 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 : 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₁
⊢ ∃ (r : k), ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
have right : p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
Tactic: use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁