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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
inr : (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
⊢ {p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s

Tactic:
apply Set.union_subset (Set.singleton_subset_iff.mpr hp)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.union_subset
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
inr inr₁ inr₂ inr₃ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
⊢ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s

Tactic:
rwa [← (Equiv.vaddConst p).subset_symm_image b s]

Premises used: Equiv.vaddConst, Equiv.subset_symm_image
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)

Tactic:
rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂

Premises used: Equiv.coe_vaddConst_symm, vectorSpan_eq_span_vsub_set_right
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
hb₄ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
⊢ AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)

Tactic:
rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂

Premises used: Equiv.coe_vaddConst_symm, vectorSpan_eq_span_vsub_set_right
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k ((⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s))
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
hb₄ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₅ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
⊢ ∀ v ∈ b, v ≠ 0

Tactic:
rw [Equiv.coe_vaddConst_symm, ← vectorSpan_eq_span_vsub_set_right k hp] at hb₂

Premises used: Equiv.coe_vaddConst_symm, vectorSpan_eq_span_vsub_set_right
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
inr :
  Eq (α := Submodule k V)
    (AffineSubspace.direction (P := P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)))
    (AffineSubspace.direction (affineSpan k s))
inr₁ :
  ((↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)).Nonempty
⊢ Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)

Tactic:
apply AffineSubspace.ext_of_direction_eq

Premises used: AffineSubspace.ext_of_direction_eq
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))

Tactic:
simp
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))

Tactic:
have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
this : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))
inr :
  Eq (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b)))
    (Submodule.span k (insert 0 b))
⊢ Eq (α := Submodule k V)
    (AffineSubspace.direction (P := P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)))
    (AffineSubspace.direction (affineSpan k s))

Tactic:
simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
        vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]

Premises used: Equiv.coe_vaddConst, direction_affineSpan, Set.singleton_union, Set.mem_insert, vectorSpan_eq_span_vsub_set_right
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
this : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))
inr : (fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b) = insert 0 b
⊢ Eq (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b)))
    (Submodule.span k (insert 0 b))

Tactic:
congr
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
this : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))
inr :
  Set.image (α := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V) (insert p ((⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) =
    insert 0 b
⊢ (fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b) = insert 0 b

Tactic:
change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _

Premises used: Equiv.vaddConst, Insert.insert, Set.image, Equiv.symm, DFunLike.coe
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
this : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))
inr :
  insert (α := V) (((Equiv.vaddConst p).symm : (a : P) → V) p : V)
      (comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V)
          (⇑(Equiv.vaddConst p) : (a : V) → P) ''
        b) =
    insert 0 b
⊢ Set.image (α := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V) (insert p ((⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) =
    insert 0 b

Tactic:
rw [Set.image_insert_eq, ← Set.image_comp]

Premises used: Set.image_comp, Set.image_insert_eq
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
this : Eq (α := Submodule k V) (Submodule.span k b) (Submodule.span k (insert 0 b))
⊢ insert (α := V) (((Equiv.vaddConst p).symm : (a : P) → V) p : V)
      (comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V)
          (⇑(Equiv.vaddConst p) : (a : V) → P) ''
        b) =
    insert 0 b

Tactic:
simp
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
h : p ∈ (↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)
⊢ ((↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)).Nonempty

Tactic:
use p
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
h : p ∈ (↑(affineSpan k (insert p ((fun (a : V) ↦ a +ᵥ p) '' b))) : Set P) ∧ p ∈ (↑(affineSpan k s) : Set P)
⊢ p ∈ (↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)

Tactic:
simp only [Equiv.coe_vaddConst, Set.singleton_union, Set.mem_inter_iff]

Premises used: Equiv.coe_vaddConst, Set.mem_inter_iff, Set.singleton_union
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ p ∈ (↑(affineSpan k (insert p ((fun (a : V) ↦ a +ᵥ p) '' b))) : Set P) ∧ p ∈ (↑(affineSpan k s) : Set P)

Tactic:
⟨mem_affineSpan k (Set.mem_insert p _), mem_affineSpan k hp⟩

Premises used: mem_affineSpan, And.intro, Set.mem_insert
-- 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 : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ (⇑(Equiv.vaddConst p).symm : (a : P) → V) '' s
hb₂ : Eq (α := Submodule k V) (Submodule.span k b) (vectorSpan k s)
hb₃ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ p ∈ (↑(affineSpan k (insert p ((fun (a : V) ↦ a +ᵥ p) '' b))) : Set P) ∧ p ∈ (↑(affineSpan k s) : Set P)

Tactic:
exact ⟨mem_affineSpan k (Set.mem_insert p _), mem_affineSpan k hp⟩
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
rw :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (Nat.succ 0).succ // x ≠ 0 }) ↦
    ![p₁, p₂] (↑i : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0
⊢ AffineIndependent k ![p₁, p₂]

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0]

Premises used: Matrix.vecEmpty, affineIndependent_iff_linearIndependent_vsub, OfNat.ofNat, Matrix.vecCons
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ Ne (α := Fin 2) 1 0

Tactic:
simp
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
i : Fin 2
hi : i ≠ 0
a : (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi) : Fin 2) : ℕ) = (↑(↑i₁ : Fin 2) : ℕ)
⊢ Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi = i₁

Tactic:
ext
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
i : Fin 2
hi : i ≠ 0
a :
  ∀ (hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 0),
    (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
      (↑(↑i₁ : Fin 2) : ℕ)
a₁ :
  ∀ (hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 0),
    (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
      (↑(↑i₁ : Fin 2) : ℕ)
⊢ (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi) : Fin 2) : ℕ) = (↑(↑i₁ : Fin 2) : ℕ)

Tactic:
fin_cases 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 0
⊢ (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
    (↑(↑i₁ : Fin 2) : ℕ)

Tactic:
simp at hi
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 0
⊢ (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
    (↑(↑i₁ : Fin 2) : ℕ)

Tactic:
simp [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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
⊢ ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁

Tactic:
have he' : ∀ i, i = i₁ := by
    rintro ⟨i, hi⟩
    ext
    fin_cases i
    · simp at hi
    · simp [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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
he' : ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁
haveI :
  ∀ (this : Unique { x : Fin 2 // x ≠ 0 }),
    LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (Nat.succ 0).succ // x ≠ 0 }) ↦
      ![p₁, p₂] (↑i : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (Nat.succ 0).succ // x ≠ 0 }) ↦
    ![p₁, p₂] (↑i : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0

Tactic:
haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
he' : ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁
this : Unique { x : Fin 2 // x ≠ 0 }
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (Nat.succ 0).succ // x ≠ 0 }) ↦
    ![p₁, p₂] (↑i : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0

Tactic:
.of_subsingleton default ?_

Premises used: Inhabited.default, LinearIndependent.of_subsingleton
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
he' : ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁
this : Unique { x : Fin 2 // x ≠ 0 }
refine : ![p₁, p₂] (↑default : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (Nat.succ 0).succ // x ≠ 0 }) ↦
    ![p₁, p₂] (↑i : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0

Tactic:
refine .of_subsingleton default ?_
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
he' : ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁
this : Unique { x : Fin 2 // x ≠ 0 }
rw : ![p₁, p₂] (↑i₁ : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0
⊢ ![p₁, p₂] (↑default : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0

Tactic:
rw [he' default]

Premises used: Inhabited.default
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
he' : ∀ (i : { x : Fin 2 // x ≠ 0 }), i = i₁
this : Unique { x : Fin 2 // x ≠ 0 }
⊢ ![p₁, p₂] (↑i₁ : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0

Tactic:
simpa using h.symm

Premises used: Ne.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 : ι)
pos : ∀ (his : i ∈ s ∧ w i ≠ 0), ∀ i ∈ s, w i = 0
neg : ∀ (his : ¬(i ∈ s ∧ w i ≠ 0)), ∀ i ∈ s, w i = 0
⊢ ∀ i ∈ s, w i = 0

Tactic:
by_cases his : i ∈ s ∧ w i ≠ 0
-- 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
⊢ ∀ i ∈ s, w i = 0

Tactic:
False.elim (hi ?_)

Premises used: False.elim
-- 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
pos : Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' {x : ι | x ≠ i})) (p i)
⊢ ∀ i ∈ s, w i = 0

Tactic:
refine False.elim (hi ?_)

Premises used: False.elim
-- 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
wm : ι → k := -(w i)⁻¹ • w
⊢ Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → k) → V) wm : V) (0 : V)

Tactic:
simp [wm, hs]