k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ AffineIndependent k ![p₁, p₂]
rw [affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0]
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
let i₁ : { x // x ≠ (0 : Fin 2) } := ⟨1, by norm_num⟩
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
case a
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ Matrix.vecCons p₁ ![p₂] ↑default -ᵥ Matrix.vecCons p₁ ![p₂] 0 ≠ 0
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ LinearIndependent k fun i => Matrix.vecCons p₁ ![p₂] ↑i -ᵥ Matrix.vecCons p₁ ![p₂] 0
apply linearIndependent_unique
case a
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ Matrix.vecCons p₁ ![p₂] ↑i₁ -ᵥ Matrix.vecCons p₁ ![p₂] 0 ≠ 0
case a
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ Matrix.vecCons p₁ ![p₂] ↑default -ᵥ Matrix.vecCons p₁ ![p₂] 0 ≠ 0
rw [he' default]
no goals
case a
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ Matrix.vecCons p₁ ![p₂] ↑i₁ -ᵥ Matrix.vecCons p₁ ![p₂] 0 ≠ 0
simpa using h.symm
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ 1 ≠ 0
norm_num
case mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
i : Fin 2
hi : i ≠ 0
⊢ { val := i, property := hi } = i₁
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
⊢ ∀ (i : { x // x ≠ 0 }), i = i₁
rintro ⟨i, hi⟩
case mk.a.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
i : Fin 2
hi : i ≠ 0
⊢ ↑↑{ val := i, property := hi } = ↑↑i₁
case mk
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
i : Fin 2
hi : i ≠ 0
⊢ { val := i, property := hi } = i₁
ext
case mk.a.h.head
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
hi : { val := 0, isLt := (_ : 0 < 2) } ≠ 0
⊢ ↑↑{ val := { val := 0, isLt := (_ : 0 < 2) }, property := hi } = ↑↑i₁

case mk.a.h.tail.head
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
hi : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ 0
⊢ ↑↑{ val := { val := 1, isLt := (_ : (fun a => a < 2) 1) }, property := hi } = ↑↑i₁
case mk.a.h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
i : Fin 2
hi : i ≠ 0
⊢ ↑↑{ val := i, property := hi } = ↑↑i₁
fin_cases i
no goals
case mk.a.h.head
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
hi : { val := 0, isLt := (_ : 0 < 2) } ≠ 0
⊢ ↑↑{ val := { val := 0, isLt := (_ : 0 < 2) }, property := hi } = ↑↑i₁
simp at hi
no goals
case mk.a.h.tail.head
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.410622
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := { val := 1, property := (_ : 1 ≠ 0) }
hi : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ 0
⊢ ↑↑{ val := { val := 1, isLt := (_ : (fun a => a < 2) 1) }, property := hi } = ↑↑i₁
simp only [Fin.val_one]