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
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
rw : AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3))
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap (1 : Fin 3) 2)]

Premises used: affineIndependent_equiv, Equiv.swap, 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₃, p₂]

Tactic:
affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₁p₃ hp₁ hp₃ hp₂

Premises used: affineIndependent_of_ne_of_mem_of_mem_of_notMem
-- 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 : ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) = ![p₁, p₃, p₂]
⊢ AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3))

Tactic:
convert! affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₁p₃ hp₁ hp₃ hp₂ using 1

Premises used: affineIndependent_of_ne_of_mem_of_mem_of_notMem
-- 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 3), (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, p₃, p₂] x
⊢ ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) = ![p₁, 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 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, ⋯⟩)
h₂ :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3)) x = ![p₁, 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 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, ⋯⟩)

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 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, ⋯⟩)

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 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 1 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    ![p₁, p₃, p₂] ((fun (i : Fin 3) ↦ i) ⟨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
rw : AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3))
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]

Premises used: affineIndependent_equiv, Equiv.swap, 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₂, p₁]

Tactic:
affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₂p₃.symm hp₃ hp₂ hp₁

Premises used: Ne.symm, affineIndependent_of_ne_of_mem_of_mem_of_notMem
-- 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 : ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) = ![p₃, p₂, p₁]
⊢ AffineIndependent k (ι := Fin 3) (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3))

Tactic:
convert! affineIndependent_of_ne_of_mem_of_mem_of_notMem hp₂p₃.symm hp₃ hp₂ hp₁ using 1

Premises used: Ne.symm, affineIndependent_of_ne_of_mem_of_mem_of_notMem
-- 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 3), (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, p₂, p₁] x
⊢ ![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) = ![p₃, 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 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, ⋯⟩)
h₂ :
  comp (α := Fin 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)
⊢ (![p₁, p₂, p₃] ∘ (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3)) x = ![p₃, 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 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, ⋯⟩)

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 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, ⋯⟩)

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 3) ![p₁, p₂, p₃] (⇑(Equiv.swap 0 2) : (a : Fin 3) → Fin 3) ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) =
    ![p₃, p₂, p₁] ((fun (i : Fin 3) ↦ i) ⟨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
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
set :
  let f := update (β := fun (a : ι) ↦ P) p i p₀;
  ∀ (hf : f = update (β := fun (a : ι) ↦ P) p i p₀), AffineIndependent k f
⊢ AffineIndependent k (update (β := fun (a : ι) ↦ P) p i p₀)

Tactic:
set f : ι → P := Function.update p i p₀ with hf

Premises used: Function.update
-- 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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h : ∀ (x : (↑{x : ι | x ≠ i} : Type u_4)), p (↑x : ι) = f (↑x : ι)
⊢ Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)

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
ι : Type u_4
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
x : (↑{x : ι | x ≠ i} : Type u_4)
⊢ p (↑x : ι) = f (↑x : ι)

Tactic:
aesop
-- 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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
⊢ Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)

Tactic:
have h₁ : (fun x : {x | x ≠ i} ↦ p x) = fun x : {x | x ≠ i} ↦ f x := by ext x; aesop
-- 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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) {x : ι | x ≠ i} a → p a = f a

Tactic:
simpa using congr_fun h₁

Premises used: congr_fun
-- 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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
⊢ p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}

Tactic:
have h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i} := Set.image_congr <| by simpa using congr_fun h₁
-- 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
inst_4 : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
h₂ : p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)

Tactic:
replace ha : AffineIndependent k fun x : {x | x ≠ i} ↦ f x := h₁ ▸ AffineIndependent.subtype ha _
-- 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
inst_4 : DecidableEq ι
p : ι → P
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
h₂ : p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
⊢ f i ∉ affineSpan k (f '' {x : ι | x ≠ i})

Tactic:
aesop
-- 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
inst_4 : DecidableEq ι
p : ι → P
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x : ι | x ≠ i})
f : ι → P := update (β := fun (a : ι) ↦ P) p i p₀
hf : f = update (β := fun (a : ι) ↦ P) p i p₀
h₁ :
  Eq (α := (x : (↑{x : ι | x ≠ i} : Type u_4)) → P) (fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ p (↑x : ι))
    fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
h₂ : p '' {x : ι | x ≠ i} = f '' {x : ι | x ≠ i}
ha : AffineIndependent.{u_1, u_2, u_3, u_4} k (P := P) fun (x : (↑{x : ι | x ≠ i} : Type u_4)) ↦ f (↑x : ι)
⊢ AffineIndependent k f

Tactic:
exact AffineIndependent.affineIndependent_of_notMem_span ha <| by aesop

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 : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) w₁ : P)
        (singleton (α := P) ((affineCombination k s p : (a : ι → k) → P) w₂ : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
rw :
  ∀ (hs : ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hi0 : w₁ i = 0)
    (hj0 : w₁ j = 0)
    (hij :
      Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
        ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
      ((SignType.sign : (a : k) → SignType) (w j) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)

Tactic:
rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs

Premises used: affineCombination_mem_affineSpan_pair
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w₂ i) 1
hs : ∃ (r : k), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w₂ i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w₂ j) : SignType)
rcases :
  ∀ (r : k) (hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i),
    Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
      ((SignType.sign : (a : k) → SignType) (w j) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i) : SignType)
    ((SignType.sign : (a : k) → SignType) (w j) : SignType)

Tactic:
rcases hs with ⟨r, hr⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k (insert (p i₁) (singleton (α := P) ((AffineMap.lineMap (p i₂) (p i₃) : (a : k) → P) c : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)

Tactic:
rw [← s.affineCombination_piSingle k p h₁, ←
      s.affineCombination_affineCombinationLineMapWeights p h₂ h₃ c] at hs

Premises used: Finset.affineCombination_affineCombinationLineMapWeights, Finset.affineCombination_piSingle
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)

Tactic:
sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_

Premises used: sign_eq_of_affineCombination_mem_affineSpan_pair, Pi.single_eq_of_ne, Ne.symm, Finset.sum_affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
refine_1 : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1
refine_2 :
  Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (affineCombinationLineMapWeights i₂ i₃ c i₃) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : k) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : k) → SignType) (w i₃) : SignType)

Tactic:
refine
      sign_eq_of_affineCombination_mem_affineSpan_pair h hw ?_
        (s.sum_affineCombinationLineMapWeights h₂ h₃ c) hs h₂ h₃
        (Pi.single_eq_of_ne h₁₂.symm _)
        (Pi.single_eq_of_ne h₁₃.symm _) ?_

Premises used: sign_eq_of_affineCombination_mem_affineSpan_pair, Pi.single_eq_of_ne, Ne.symm, Finset.sum_affineCombinationLineMapWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup V
inst_4 : Module k V
inst_5 : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, w i) 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  Membership.mem (α := P) (γ := AffineSubspace k P)
    (affineSpan k
      (insert (α := P) ((affineCombination k s p : (a : ι → k) → P) (Pi.single (M := fun (a : ι) ↦ k) i₁ 1) : P)
        (singleton (α := P)
          ((affineCombination k s p : (a : ι → k) → P) (affineCombinationLineMapWeights i₂ i₃ c) : P))))
    ((affineCombination k s p : (a : ι → k) → P) w : P)
refine_1 : Eq.{u_1 + 1} (α := k) (if i₁ ∈ s then 1 else 0) 1
refine_1₁ refine_1₂ : Eq.{u_1 + 1} (α := k) 1 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, Pi.single (M := fun (a : ι) ↦ k) i₁ 1 i) 1

Tactic:
rw [Finset.sum_pi_single', if_pos h₁]

Premises used: if_pos, Finset.sum_pi_single'