awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ AffineIndependent k p
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ AffineIndependent k p
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
have 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 }))
Tactic: rw [← affineIndependent_equiv (finSuccAboveEquiv (2 : Fin 3))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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) (ι := 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 }))
have 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₂]
Tactic: convert! affineIndependent_of_ne k hp₁p₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ (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₂]
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ ((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
have 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, sorry⟩) =
  ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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))
⊢ ((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
have 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, sorry⟩) =
  ![p₁, p₂] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
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₂, p₃]
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₃]
have refine : ![p₁, p₂, p₃] 2 ∉ affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2})
Tactic: refine ha.affineIndependent_of_notMem_span ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
have refine : affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2}) ≤ s
Tactic: refine hp₃ ((AffineSubspace.le_def' _ s).1 ?_ p₃ h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
⊢ affineSpan k (![p₁, p₂, p₃] '' {x : Fin 3 | x ≠ 2}) ≤ s
have simp_rw : ∀ (x : Fin 3), Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)
Tactic: simp_rw [affineSpan_le, Set.image_subset_iff, Set.subset_def, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)
have 0 : Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩) →
  ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) ∈ (↑s : Set P)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)
have 1 : Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩) →
  ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) ∈ (↑s : Set P)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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)
⊢ Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} x → ![p₁, p₂, p₃] x ∈ (↑s : Set P)
have 2 : Membership.mem (γ := Set (Fin 3)) {x : Fin 3 | x ≠ 2} ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩) →
  ![p₁, p₂, p₃] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) ∈ (↑s : Set P)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂, p₃]
have rw : AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3))
Tactic: rw [← affineIndependent_equiv (Equiv.swap (1 : Fin 3) 2)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3))
have h : ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) = ![p₁, p₃, p₂]
Tactic: convert! affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₁p₃ hp₁ hp₃ hp₂ using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) = ![p₁, p₃, p₂]
have h : ∀ (x : Fin 3), (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, p₃, p₂] x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, p₃, p₂] x
have h : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) =
  ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
h :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, p₃, p₂] x
have h₁ : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) =
  ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
h :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
h₁ :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, p₃, p₂] x
have h₂ : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) =
  ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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₂, p₃]
have rw : AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3))
Tactic: rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3))
have h : ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) = ![p₃, p₂, p₁]
Tactic: convert! affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₂p₃.symm hp₃ hp₂ hp₁ using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
⊢ ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) = ![p₃, p₂, p₁]
have h : ∀ (x : Fin 3), (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, p₂, p₁] x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, p₂, p₁] x
have h : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) =
  ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
h :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, p₂, p₁] x
have h₁ : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) =
  ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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 3
h :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) =
    ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)
h₁ :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) =
    ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, p₂, p₁] x
have h₂ : comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) =
  ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
⊢ AffineIndependent k (update (β := fun (a : ι) ↦ P) p i p₀)
have set : let f := update (β := fun (a : ι) ↦ P) p i p₀;
∀ (hf : f = update (β := fun (a : ι) ↦ P) p i p₀), AffineIndependent k f
Tactic: set f : ι → P := Function.update p i p₀ with hf