awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))

Tactic:
le_antisymm ?_ (Submodule.span_mono ?_)

Premises used: le_antisymm, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))
refine_2 : (fun (x : P) ↦ p -ᵥ x) '' s ⊆ s -ᵥ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))

Tactic:
refine le_antisymm ?_ (Submodule.span_mono ?_)

Premises used: le_antisymm, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
refine_1 : s -ᵥ s ⊆ (↑(Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s)) : Set V)
⊢ LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = v
⊢ p -ᵥ p₂ - (p -ᵥ p₁) = v

Tactic:
simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv

Premises used: vsub_sub_vsub_cancel_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
refine_1 : ∀ (p_1 : Submodule k V), (fun (x : P) ↦ p -ᵥ x) '' s ⊆ (↑p_1 : Set V) → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' s)) : Set V)

Tactic:
rw [← hv, SetLike.mem_coe, Submodule.mem_span]

Premises used: SetLike.mem_coe, Submodule.mem_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ ∀ (p_1 : Submodule k V), (fun (x : P) ↦ p -ᵥ x) '' s ⊆ (↑p_1 : Set V) → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1

Tactic:
fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)

Premises used: And.intro, Exists.intro, rfl, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ ∀ (p_1 : Submodule k V), (fun (x : P) ↦ p -ᵥ x) '' s ⊆ (↑p_1 : Set V) → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1

Tactic:
exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x : P) ↦ p -ᵥ x) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
⟨p, hp, p₂, hp₂, hv⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x : P) ↦ p -ᵥ x) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
exact ⟨p, hp, p₂, hp₂, hv⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))

Tactic:
le_antisymm ?_ (Submodule.span_mono ?_)

Premises used: le_antisymm, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
refine_1 : LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))
refine_2 : (fun (x : P) ↦ x -ᵥ p) '' s ⊆ s -ᵥ s
⊢ Eq (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))

Tactic:
refine le_antisymm ?_ (Submodule.span_mono ?_)

Premises used: le_antisymm, Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
refine_1 : s -ᵥ s ⊆ (↑(Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s)) : Set V)
⊢ LE.le (α := Submodule k V) (Submodule.span k (s -ᵥ s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s))

Tactic:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x1 x2 : P) ↦ x1 -ᵥ x2) p₁ p₂ = v
⊢ p₁ -ᵥ p - (p₂ -ᵥ p) = v

Tactic:
simp_rw [← vsub_sub_vsub_cancel_right p₁ p₂ p] at hv

Premises used: vsub_sub_vsub_cancel_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
refine_1 : ∀ (p_1 : Submodule k V), (fun (x : P) ↦ x -ᵥ p) '' s ⊆ (↑p_1 : Set V) → p₁ -ᵥ p - (p₂ -ᵥ p) ∈ p_1
⊢ v ∈ (↑(Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' s)) : Set V)

Tactic:
rw [← hv, SetLike.mem_coe, Submodule.mem_span]

Premises used: SetLike.mem_coe, Submodule.mem_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ ∀ (p_1 : Submodule k V), (fun (x : P) ↦ x -ᵥ p) '' s ⊆ (↑p_1 : Set V) → p₁ -ᵥ p - (p₂ -ᵥ p) ∈ p_1

Tactic:
fun m hm => Submodule.sub_mem _ (hm ⟨p₁, hp₁, rfl⟩) (hm ⟨p₂, hp₂, rfl⟩)

Premises used: And.intro, Exists.intro, rfl, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ ∀ (p_1 : Submodule k V), (fun (x : P) ↦ x -ᵥ p) '' s ⊆ (↑p_1 : Set V) → p₁ -ᵥ p - (p₂ -ᵥ p) ∈ p_1

Tactic:
exact fun m hm => Submodule.sub_mem _ (hm ⟨p₁, hp₁, rfl⟩) (hm ⟨p₂, hp₂, rfl⟩)

Premises used: Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x : P) ↦ x -ᵥ p) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
⟨p₂, hp₂, p, hp, hv⟩

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun (x : P) ↦ x -ᵥ p) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
exact ⟨p₂, hp₂, p, hp, hv⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
rw : Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))
| vectorSpan k s

Tactic:
rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, vectorSpan_eq_span_vsub_set_left, Set.insert_diff_singleton, Set.image_insert_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
conv_lhs :
  Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p}))))
    (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))
⊢ Eq (α := Submodule k V) (vectorSpan k s) (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, vectorSpan_eq_span_vsub_set_left, Set.insert_diff_singleton, Set.image_insert_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p}))))
    (Submodule.span k ((fun (x : P) ↦ p -ᵥ x) '' (s \ {p})))

Tactic:
simp [Submodule.span_insert_eq_span]

Premises used: Submodule.span_insert_eq_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
rw : Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))
| vectorSpan k s

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton, Set.image_insert_eq, vectorSpan_eq_span_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
conv_lhs :
  Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p}))))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))
⊢ Eq (α := Submodule k V) (vectorSpan k s) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_diff_singleton, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton, Set.image_insert_eq, vectorSpan_eq_span_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (insert (p -ᵥ p) ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p}))))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' (s \ {p})))

Tactic:
simp [Submodule.span_insert_eq_span]

Premises used: Submodule.span_insert_eq_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
inst_4 : DecidableEq P
inst_5 : DecidableEq V
s : Finset P
p : P
hp : p ∈ s
⊢ Eq (α := Submodule k V) (vectorSpan k (↑s : Set P))
    (Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p) (s.erase p)) : Set V))

Tactic:
simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]

Premises used: Iff.mpr, vectorSpan_eq_span_vsub_set_right_ne, Finset.mem_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
rw : Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))
| vectorSpan k (p '' s)

Tactic:
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, vectorSpan_eq_span_vsub_set_left, Set.mem_image_of_mem, Set.insert_diff_singleton, Set.image_insert_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
conv_lhs :
  Eq (α := Submodule k V) (Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i}))))
    (Submodule.span k ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s)) (Submodule.span k ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi, ←
      Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, vectorSpan_eq_span_vsub_set_left, Set.mem_image_of_mem, Set.insert_diff_singleton, Set.image_insert_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i}))))
    (Submodule.span k ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))

Tactic:
simp [Submodule.span_insert_eq_span]

Premises used: Submodule.span_insert_eq_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
rw : Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))
| vectorSpan k (p '' s)

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi,
      ← Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, Set.mem_image_of_mem, Set.insert_diff_singleton, Set.image_insert_eq, vectorSpan_eq_span_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
conv_lhs :
  Eq (α := Submodule k V) (Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i}))))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi,
      ← Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Premises used: Set.insert_eq_of_mem, Set.mem_image_of_mem, Set.insert_diff_singleton, Set.image_insert_eq, vectorSpan_eq_span_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
s : Set ι
i : ι
hi : i ∈ s
⊢ Eq (α := Submodule k V) (Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i}))))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))

Tactic:
simp [Submodule.span_insert_eq_span]

Premises used: Submodule.span_insert_eq_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i0 : ι
rw :
  Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k (range ((fun (x : P) ↦ p i0 -ᵥ x) ∘ p)))
    (Submodule.span k (range fun (i : ι) ↦ p i0 -ᵥ p i))
⊢ Eq (α := Submodule k V) (vectorSpan k (range p)) (Submodule.span k (range fun (i : ι) ↦ p i0 -ᵥ p i))

Tactic:
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]

Premises used: Set.mem_range_self, Set.range_comp, vectorSpan_eq_span_vsub_set_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i0 : ι
⊢ Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k (range ((fun (x : P) ↦ p i0 -ᵥ x) ∘ p)))
    (Submodule.span k (range fun (i : ι) ↦ p i0 -ᵥ p i))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i0 : ι
rw :
  Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k (range ((fun (x : P) ↦ x -ᵥ p i0) ∘ p)))
    (Submodule.span k (range fun (i : ι) ↦ p i -ᵥ p i0))
⊢ Eq (α := Submodule k V) (vectorSpan k (range p)) (Submodule.span k (range fun (i : ι) ↦ p i -ᵥ p i0))

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]

Premises used: Set.mem_range_self, Set.range_comp, vectorSpan_eq_span_vsub_set_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i0 : ι
⊢ Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k (range ((fun (x : P) ↦ x -ᵥ p i0) ∘ p)))
    (Submodule.span k (range fun (i : ι) ↦ p i -ᵥ p i0))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
rw :
  Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ p i₀ -ᵥ x) '' p '' (univ \ {i₀})))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)))
⊢ Eq (α := Submodule k V) (vectorSpan k (range p))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)))

Tactic:
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]

Premises used: Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
e_s :
  ∀ (v : V),
    Membership.mem (γ := Set V) ((fun (x : P) ↦ p i₀ -ᵥ x) '' p '' (univ \ {i₀})) v ↔
      Membership.mem (γ := Set V) (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)) v
⊢ Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ p i₀ -ᵥ x) '' p '' (univ \ {i₀})))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)))

Tactic:
congr with v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
e_s :
  (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔
    ∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ p i₀ -ᵥ x) '' p '' (univ \ {i₀})) v ↔
    Membership.mem (γ := Set V) (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)) v

Tactic:
simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists]

Premises used: Set.mem_range, Set.mem_image, Subtype.exists, Set.mem_singleton_iff, Set.mem_diff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
e_s :
  (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) →
    ∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v
e_s₁ :
  (∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v) →
    ∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v
⊢ (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔
    ∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
i₁ : ι
left : Membership.mem (γ := Set ι) univ i₁
hi₁ : ¬i₁ = i₀
hv : p i₀ -ᵥ p i₁ = v
⊢ ∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v

Tactic:
⟨i₁, hi₁, hv⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
i₁ : ι
left : Membership.mem (γ := Set ι) univ i₁
hi₁ : ¬i₁ = i₀
hv : p i₀ -ᵥ p i₁ = v
⊢ ∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v

Tactic:
exact ⟨i₁, hi₁, hv⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
⊢ (∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v) →
    ∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

Premises used: Set.univ, Membership.mem, Exists, VSub.vsub, And, And.intro, Exists.intro, Set.mem_univ, Eq, Not, rfl, _private.0.vectorSpan_range_eq_span_range_vsub_left_ne.match_5
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
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
i₀ : ι
v : V
⊢ (∃ (a : ι) (_ : a ≠ i₀), p i₀ -ᵥ p a = v) →
    ∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩