k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
⊢ AffineIndependent k ![p₁, p₂, p₃]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ AffineIndependent k ![p₁, p₂, p₃]
have ha : AffineIndependent k fun x : { x : Fin 3 // x ≠ 2 } => ![p₁, p₂, p₃] x := by
  rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3)).toEquiv]
  convert affineIndependent_of_ne k hp₁p₂
  ext x
  fin_cases x <;> rfl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
⊢ ¬Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
⊢ AffineIndependent k ![p₁, p₂, p₃]
refine' ha.affineIndependent_of_not_mem_span _
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ False
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
⊢ ¬Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
intro h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2}) ≤ s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ False
refine' hp₃ ((AffineSubspace.le_def' _ s).1 _ p₃ h)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ (x : Fin 3), x ∈ {x | x ≠ 2} → Matrix.vecCons p₁ ![p₂, p₃] x ∈ ↑s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2}) ≤ s
simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
x : Fin 3
⊢ x ∈ {x | x ≠ 2} → Matrix.vecCons p₁ ![p₂, p₃] x ∈ ↑s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
⊢ ∀ (x : Fin 3), x ∈ {x | x ≠ 2} → Matrix.vecCons p₁ ![p₂, p₃] x ∈ ↑s
intro x
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
ha : AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
h : Matrix.vecCons p₁ ![p₂, p₃] 2 ∈ affineSpan k (![p₁, p₂, p₃] '' {x | x ≠ 2})
x : Fin 3
⊢ x ∈ {x | x ≠ 2} → Matrix.vecCons p₁ ![p₂, p₃] x ∈ ↑s
fin_cases x <;> simp [hp₁, hp₂]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ AffineIndependent k ((fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ AffineIndependent k fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x
rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3)).toEquiv]
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ (fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv = ![p₁, p₂]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ AffineIndependent k ((fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv)
convert affineIndependent_of_ne k hp₁p₂
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
x : Fin 2
⊢ ((fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv) x = Matrix.vecCons p₁ ![p₂] x
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
⊢ (fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv = ![p₁, p₂]
ext x
no goals
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.444767
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : ¬p₃ ∈ s
x : Fin 2
⊢ ((fun x => Matrix.vecCons p₁ ![p₂, p₃] ↑x) ∘ ↑(finSuccAboveEquiv 2).toEquiv) x = Matrix.vecCons p₁ ![p₂] x
fin_cases x <;> rfl