k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.280484
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.280484
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by
  fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp only at h₁₂ h₁₃ h₂₃ ⊢
no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.280484
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
  Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type ?u.280484
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Finset.univ = {i₁, i₂, i₃}
fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp only at h₁₂ h₁₃ h₂₃ ⊢