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 : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : 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
c : k
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w : P)
      (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
                ((affineCombination k s p : (a : ι → k) → P) w₂) :
              k →ᵃ[k] P) :
            (a : k) → P)
          c :
        P) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c
have rw : (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) ↔
  ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c
Tactic: rw [← AffineMap.apply_lineMap, ha.affineCombination_eq_iff_eq hw]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : 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
c : k
rw :
  (∀ i ∈ s, w i = (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c
⊢ Eq.{u_3 + 1} (α := P) ((affineCombination k s p : (a : ι → k) → P) w : P)
      (((AffineMap.lineMap ((affineCombination k s p : (a : ι → k) → P) w₁)
                ((affineCombination k s p : (a : ι → k) → P) w₂) :
              k →ᵃ[k] P) :
            (a : k) → P)
          c :
        P) ↔
    ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i) : (a : k) → k) c
have rw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, (AffineMap.lineMap w₁ w₂ : (a : k) → ι → k) c i) 1
Tactic: rw [← AffineMap.apply_lineMap, ha.affineCombination_eq_iff_eq hw]
-- 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 : Set P
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have inl : ∃ t ⊆ ∅,
  Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k ∅) ∧
    AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t }) (Subtype.val (p := fun (x : P) ↦ x ∈ t))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
Cleared hypotheses: s
-- 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 : Set P
inl :
  ∃ t ⊆ ∅,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k ∅) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have inr : ∀ (p : P) (hp : p ∈ s),
  ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
-- 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 : Set P
p : P
hp : p ∈ s
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have inr : ∀ (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₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))),
  ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
Tactic: obtain ⟨b, hb₁, hb₂, hb₃⟩ := exists_linearIndependent k ((Equiv.vaddConst p).symm '' s)
-- 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 : 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₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have hb₀ : ∀ v ∈ b, v ≠ 0
Tactic: have hb₀ : ∀ v : V, v ∈ b → v ≠ 0 := fun v hv => hb₃.ne_zero (⟨v, hv⟩ : b)
-- 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 : 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₃ : LinearIndependent.{u_2, u_1, u_2} (ι := { x : V // x ∈ b }) k (Subtype.val (p := fun (x : V) ↦ x ∈ b))
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have hb₄ : AffineIndependent k (P := P) fun (p_1 : (↑({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' b) : Type u_3)) ↦ (↑p_1 : P)
Tactic: rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k hb₀ p] at hb₃
Cleared hypotheses: hb₃, hb₀
-- 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 : 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
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have inr : {p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
Tactic: refine ⟨{p} ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩
-- 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 : 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 : {p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
⊢ ∃ t ⊆ s,
    Eq (α := AffineSubspace k P) (affineSpan k t) (affineSpan k s) ∧
      AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ t })
        (Subtype.val (p := fun (x : P) ↦ x ∈ t))
have inr₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)
Tactic: refine ⟨{p} ∪ Equiv.vaddConst p '' b, ?_, ?_, hb₃⟩
-- 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 : 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
⊢ {p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
have inr : (⇑(Equiv.vaddConst p) : (a : V) → P) '' b ⊆ s
Tactic: apply Set.union_subset (Set.singleton_subset_iff.mpr hp)
-- 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 : 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 (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)
have hb₄ : 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₂
Cleared hypotheses: hb₂, hb₃, hb₀
-- 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 : 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 (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)
have inr : Eq (α := Submodule k V)
  (AffineSubspace.direction (P := P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)))
  (AffineSubspace.direction (affineSpan k s))
Tactic: apply AffineSubspace.ext_of_direction_eq
-- 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 : 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))
⊢ Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) (affineSpan k s)
have inr₁ : ((↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)).Nonempty
Tactic: apply AffineSubspace.ext_of_direction_eq
-- 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 : 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)
    (AffineSubspace.direction (P := P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)))
    (AffineSubspace.direction (affineSpan k s))
have this : 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
-- 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 : 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))
⊢ Eq (α := Submodule k V)
    (AffineSubspace.direction (P := P) (affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)))
    (AffineSubspace.direction (affineSpan k s))
have 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))
Tactic: simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
        vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]
-- 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 : 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))
⊢ 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))
have inr : (fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b) = insert 0 b
Tactic: congr
-- 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 : 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))
⊢ (fun (x : P) ↦ x -ᵥ p) '' insert p ((fun (a : V) ↦ a +ᵥ p) '' b) = insert 0 b
have inr : Set.image (α := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V) (insert p ((⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) =
  insert 0 b
Tactic: change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _
-- 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 : 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))
⊢ Set.image (α := P) (⇑(Equiv.vaddConst p).symm : (a : P) → V) (insert p ((⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) =
    insert 0 b
have 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
Tactic: rw [Set.image_insert_eq, ← Set.image_comp]
-- 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 : 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
⊢ ((↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)).Nonempty
have h : p ∈ (↑(affineSpan k ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)
Tactic: use 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 : 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 ({p} ∪ (⇑(Equiv.vaddConst p) : (a : V) → P) '' b)) : Set P) ∩ (↑(affineSpan k s) : Set P)
have h : p ∈ (↑(affineSpan k (insert p ((fun (a : V) ↦ a +ᵥ p) '' b))) : Set P) ∧ p ∈ (↑(affineSpan k s) : Set P)
Tactic: simp only [Equiv.coe_vaddConst, Set.singleton_union, Set.mem_inter_iff]
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
⊢ AffineIndependent k ![p₁, p₂]
have 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
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k ![p₁, p₂] 0]
-- 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
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
⊢ Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi = i₁
have a : (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi) : Fin 2) : ℕ) = (↑(↑i₁ : Fin 2) : ℕ)
Tactic: ext
-- 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
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
⊢ (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi) : Fin 2) : ℕ) = (↑(↑i₁ : Fin 2) : ℕ)
have a : ∀ (hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 0),
  (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
    (↑(↑i₁ : Fin 2) : ℕ)
Tactic: fin_cases i
Cleared hypotheses: i, hi
-- 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
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) : ℕ)
⊢ (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) i hi) : Fin 2) : ℕ) = (↑(↑i₁ : Fin 2) : ℕ)
have a₁ : ∀ (hi : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 0),
  (↑(↑(Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) hi) : Fin 2) : ℕ) =
    (↑(↑i₁ : Fin 2) : ℕ)
Tactic: fin_cases i
Cleared hypotheses: i, hi
-- 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
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x : Fin 2 // x ≠ 0 } := Subtype.mk (p := fun (x : Fin 2) ↦ x ≠ 0) 1 ⋯
⊢ 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
have he' : ∀ (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₁]
-- 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
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₁
⊢ 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
have 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
Tactic: haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
-- 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
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
have refine : ![p₁, p₂] (↑default : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0
Tactic: refine .of_subsingleton default ?_
-- 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
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₂] (↑default : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0
have rw : ![p₁, p₂] (↑i₁ : Fin (Nat.succ 0).succ) -ᵥ ![p₁, p₂] 0 ≠ 0
Tactic: rw [he' default]
-- 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})
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 : ι)
⊢ ∀ i ∈ s, w i = 0
have pos : ∀ (his : i ∈ s ∧ w i ≠ 0), ∀ i ∈ s, w i = 0
Tactic: by_cases his : i ∈ s ∧ w i ≠ 0