awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
x : ι
hxs : x ∈ s
hwx : w x ≠ 0
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
hi : p x ∉ affineSpan k (p '' {x_1 : ι | x_1 ≠ x})
s' : Finset { y : ι // y ≠ x } := Finset.subtype (fun (x_1 : ι) ↦ x_1 ≠ x) s
p' : { y : ι // y ≠ x } → P := fun (x_1 : { y : ι // y ≠ x }) ↦ p (↑x_1 : ι)
his : x ∉ s ∨ w x = 0
w' : { y : ι // y ≠ x } → k := fun (x_1 : { y : ι // y ≠ x }) ↦ w (↑x_1 : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
⊢ False

Tactic:
exact hwx (his.neg_resolve_left hxs)

Premises used: Or.neg_resolve_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
⊢ Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)

Tactic:
have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : j ∈ s
pos : ∀ (hji : j = i), w j = 0
neg : ∀ (hji : ¬j = i), w j = 0
⊢ w j = 0

Tactic:
by_cases hji : j = i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : j ∈ s
hji : j = i
⊢ i ∈ s

Tactic:
rw [hji] at hj
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : j ∈ s
hji : j = i
hj₁ : i ∈ s
⊢ j = i

Tactic:
rw [hji] at hj
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : i ∈ s
hji : j = i
⊢ w j = 0

Tactic:
hji.symm ▸ his.neg_resolve_left hj

Premises used: Eq.rec, Or.neg_resolve_left, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : i ∈ s
hji : j = i
⊢ w j = 0

Tactic:
exact hji.symm ▸ his.neg_resolve_left hj
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : j ∈ s
hji : ¬j = i
⊢ w j = 0

Tactic:
ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

Premises used: Iff.mpr, Subtype.mk, Finset.mem_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
s : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0
hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)
s' : Finset { y : ι // y ≠ i } := Finset.subtype (fun (x : ι) ↦ x ≠ i) s
p' : { y : ι // y ≠ i } → P := fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
his : i ∉ s ∨ w i = 0
w' : { y : ι // y ≠ i } → k := fun (x : { y : ι // y ≠ i }) ↦ w (↑x : ι)
hw' : Eq.{u_1 + 1} (α := k) (∑ x ∈ s', w' x) 0
hs' : Eq.{u_2 + 1} (α := V) ((s'.weightedVSub p' : (a : { y : ι // y ≠ i } → k) → V) w' : V) (0 : V)
j : ι
hj : j ∈ s
hji : ¬j = i
⊢ w j = 0

Tactic:
exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

Premises used: Iff.mpr, Subtype.mk, Finset.mem_subtype
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : { y : ι // y ≠ i }) ↦ p (↑x : ι)
hi : p i ∉ affineSpan k (p '' {x : ι | x ≠ i})
intro intro₁ intro₂ intro₃ :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)), ∀ i ∈ s, w i = 0
intro₄ intro₅ :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)), ∀ i ∈ s, w i = 0
pos :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)) (his : i ∈ s ∧ w i ≠ 0),
    ∀ i ∈ s, w i = 0
neg neg₁ :
  ∀ (s : Finset ι) (w : ι → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) w : V) (0 : V)) (his : ¬(i ∈ s ∧ w i ≠ 0)),
    ∀ i ∈ s, w i = 0
⊢ AffineIndependent k p

Tactic:
classical
    intro s w hw hs
    let s' : Finset { y // y ≠ i } := s.subtype (· ≠ i)
    let p' : { y // y ≠ i } → P := fun x => p x
    by_cases his : i ∈ s ∧ w i ≠ 0
    · refine False.elim (hi ?_)
      let wm : ι → k := -(w i)⁻¹ • w
      have hms : s.weightedVSub p wm = (0 : V) := by simp [wm, hs]
      have hwm : ∑ i ∈ s, wm i = 0 := by simp [wm, ← Finset.mul_sum, hw]
      have hwmi : wm i = -1 := by simp [wm, his.2]
      let w' : { y // y ≠ i } → k := fun x => wm x
      have hw' : ∑ x ∈ s', w' x = 1 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [← s.sum_filter_add_sum_filter_not (· ≠ i)] at hwm
        simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm
      rw [← s.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one hms his.1 hwmi, ←
        (Subtype.range_coe : _ = { x | x ≠ i }), ← Set.range_comp, ←
        s.affineCombination_subtype_eq_filter]
      exact affineCombination_mem_affineSpan hw' p'
    · rw [not_and_or, Classical.not_not] at his
      let w' : { y // y ≠ i } → k := fun x => w x
      have hw' : ∑ x ∈ s', w' x = 0 := by
        simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
        rw [Finset.sum_filter_of_ne, hw]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      have hs' : s'.weightedVSub p' w' = (0 : V) := by
        simp_rw [w', s', p', Finset.weightedVSub_subtype_eq_filter]
        rw [Finset.weightedVSub_filter_of_ne, hs]
        rintro x hxs hwx rfl
        exact hwx (his.neg_resolve_left hxs)
      intro j hj
      by_cases hji : j = i
      · rw [hji] at hj
        exact hji.symm ▸ his.neg_resolve_left hj
      · exact ha s' w' hw' hs' ⟨j, hji⟩ (Finset.mem_subtype.2 hj)

Premises used: Set.range_comp, Classical.not_not, False.elim, Subtype.range_coe, not_and_or
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
rw :
  AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) (ι := Fin 2)
    ((fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }))
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)

Tactic:
rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]

Premises used: affineIndependent_equiv, finSuccAboveEquiv, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
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₂]

Tactic:
affineIndependent_of_ne k hp₁p₂

Premises used: affineIndependent_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
h :
  (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) =
    ![p₁, p₂]
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) (ι := Fin 2)
    ((fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }))

Tactic:
convert! affineIndependent_of_ne k hp₁p₂

Premises used: affineIndependent_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
h :
  ∀ (x : Fin 2),
    ((fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
          (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }))
        x =
      ![p₁, p₂] x
⊢ (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) =
    ![p₁, p₂]

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
x : Fin 2
h :
  comp (α := Fin 2) (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3))
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
h₁ :
  comp (α := Fin 2) (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3))
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ ((fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)) ∘
        (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }))
      x =
    ![p₁, p₂] x

Tactic:
fin_cases x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ comp (α := Fin 2) (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3))
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ comp (α := Fin 2) (fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3))
      (⇑(finSuccAboveEquiv 2) : (a : Fin 2) → { x : Fin (2 + 1) // x ≠ 2 }) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)

Tactic:
have ha : AffineIndependent k fun x : { x : Fin 3 // x ≠ 2 } => ![p₁, p₂, p₃] x := by
    rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]
    convert! affineIndependent_of_ne k hp₁p₂
    ext x
    fin_cases x <;> rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
ha.affineIndependent_of_notMem_span ?_

Premises used: AffineIndependent.affineIndependent_of_notMem_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
refine : ![p₁, p₂, p₃] 2 ∉ affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
refine ha.affineIndependent_of_notMem_span ?_

Premises used: AffineIndependent.affineIndependent_of_notMem_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
⊢ False

Tactic:
hp₃ ((AffineSubspace.le_def' _ s).1 ?_ p₃ h)

Premises used: AffineSubspace.le_def', Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
refine : affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2}) ≤ s
⊢ False

Tactic:
refine hp₃ ((AffineSubspace.le_def' _ s).1 ?_ p₃ h)

Premises used: AffineSubspace.le_def', Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
simp_rw : ∀ (x : Fin 3), Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)
⊢ affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2}) ≤ s

Tactic:
simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage]

Premises used: Set.subset_def, affineSpan_le, Set.image_subset_iff, Set.mem_preimage
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
x : Fin 3
0 :
  Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)
1 :
  Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)
2 :
  Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)

Tactic:
fin_cases x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)

Tactic:
simp +decide [hp₁, hp₂]

Premises used: Decidable.decide
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)

Tactic:
simp +decide [hp₁, hp₂]

Premises used: Decidable.decide
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∉ s
ha : AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (x : { x : Fin 3 // x ≠ 2 }) ↦ ![p₁, p₂, p₃] (↑x : Fin 3)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})) (![p₁, p₂, p₃] 2)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) →
    ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) ∈ (↑s : Set P)

Tactic:
simp +decide [hp₁, hp₂]

Premises used: Decidable.decide