awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set ι
i : ι
hi : i ∈ s
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s)) (Submodule.span k ((fun (x : P) ↦ p i -ᵥ x) '' p '' (s \ {i})))
have 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})))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)
have rw : Submodule.span k (insert (p i -ᵥ p i) ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set ι
i : ι
hi : i ∈ s
⊢ Eq (α := Submodule k V) (vectorSpan k (p '' s)) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i) '' p '' (s \ {i})))
have 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})))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i0 : ι
⊢ Eq (α := Submodule k V) (vectorSpan k (range p)) (Submodule.span k (range fun (i : ι) ↦ p i0 -ᵥ p i))
have 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))
Tactic: rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i0 : ι
⊢ Eq (α := Submodule k V) (vectorSpan k (range p)) (Submodule.span k (range fun (i : ι) ↦ p i -ᵥ p i0))
have 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))
Tactic: rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
⊢ Eq (α := Submodule k V) (vectorSpan k (range p))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p i₀ -ᵥ p (↑i : ι)))
have 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 : ι)))
Tactic: rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
⊢ 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 : ι)))
have 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
Tactic: congr with v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
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
have 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
Tactic: simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
v : 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
⊢ Eq (α := Submodule k V) (vectorSpan k (range p))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀))
have rw : Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i₀) '' p '' (univ \ {i₀})))
  (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀))
Tactic: rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_right_ne k _ (Set.mem_univ i₀)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
⊢ Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ x -ᵥ p i₀) '' p '' (univ \ {i₀})))
    (Submodule.span k (range fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀))
have e_s : ∀ (v : V),
  Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p i₀) '' p '' (univ \ {i₀})) v ↔
    Membership.mem (γ := Set V) (range fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀) v
Tactic: congr with v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
v : V
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p i₀) '' p '' (univ \ {i₀})) v ↔
    Membership.mem (γ := Set V) (range fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀) v
have e_s : (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) ↔
  ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
Tactic: simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
v : V
⊢ (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) ↔
    ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
have e_s : (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) →
  ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
i₀ : ι
v : V
e_s :
  (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) →
    ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
⊢ (∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) ↔
    ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
have e_s₁ : (∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v) →
  ∃ (x : P), (∃ (x_1 : ι), (Membership.mem (γ := Set ι) univ x_1 ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
A : Set P
inst_4 : Nonempty.{u_3 + 1} (↑A : Type u_3)
⊢ Eq (α := AffineSubspace k ↥(affineSpan k A))
    (affineSpan k (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
    ⊤
have rw : LE.le (α := AffineSubspace k ↥(affineSpan k A)) ⊤
  (affineSpan k (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
A : Set P
inst_4 : Nonempty.{u_3 + 1} (↑A : Type u_3)
x : P
hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x
⊢ Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
    (affineSpan k (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) x hx)
have refine_1 : ∀ (y : P) (hy : y ∈ A),
  Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
    (affineSpan k (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) y sorry)
Tactic: refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
A : Set P
inst_4 : Nonempty.{u_3 + 1} (↑A : Type u_3)
x : P
hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x
refine_1 :
  ∀ (y : P) (hy : y ∈ A),
    Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
      (affineSpan k
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
      (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) y ⋯)
⊢ Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
    (affineSpan k (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) x hx)
have refine_2 : ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k A) u) (v : P)
  (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k A) v) (w : P)
  (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k A) w),
  Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
      (affineSpan k
        (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
      (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) u hu) →
    Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
        (affineSpan k
          (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
        (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) v hv) →
      Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
          (affineSpan k
            (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
          (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) w hw) →
        Membership.mem (γ := AffineSubspace k ↥(affineSpan k A))
          (affineSpan k
            (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x) ⁻¹' A))
          (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace k P) (affineSpan k A) x)
            (c • (u -ᵥ v) +ᵥ w) sorry)
Tactic: refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set V
p : P
h :
  Eq.{u_2 + 1} (α := Submodule k V)
    (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s)))) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)) ⊤
have convert_1 : Eq (α := Submodule k V) (direction (P := P) (affineSpan k ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)))
  (direction.{u_1, u_2, u_3} (P := P) ⊤)
Tactic: convert!
    ext_of_direction_eq _
      ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set V
p : P
h :
  Eq.{u_2 + 1} (α := Submodule k V)
    (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s)))) ⊤
⊢ Eq (α := Submodule k V) (direction (P := P) (affineSpan k ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)))
    (direction.{u_1, u_2, u_3} (P := P) ⊤)
have convert_1 : LE.le.{u_2} (α := Submodule k V)
  (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s))))
  (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)))
Tactic: rw [direction_affineSpan, direction_top,
    vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _),
    eq_top_iff, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set V
p : P
h :
  Eq.{u_2 + 1} (α := Submodule k V)
    (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s)))) ⊤
⊢ LE.le.{u_2} (α := Submodule k V)
    (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s))))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ p) '' ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)))
have convert_1 : Subset.{u_2} (α := Set V) (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s)))
  ((fun (x : P) ↦ x -ᵥ p) '' ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s))
Tactic: apply Submodule.span_mono
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
s : Set V
p : P
h :
  Eq.{u_2 + 1} (α := Submodule k V)
    (Submodule.span k (range (ι := { x : V // x ∈ s }) (Subtype.val (p := fun (x : V) ↦ x ∈ s)))) ⊤
v' : { x : V // x ∈ s }
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)) (↑v' : V)
have h₁ : Membership.mem (γ := Set P) ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s) ((↑v' : V) +ᵥ p) ∧
  (fun (x : P) ↦ x -ᵥ p) ((↑v' : V) +ᵥ p) = (↑v' : V)
Tactic: use (v' : V) +ᵥ p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₁ -ᵥ p₂))
have simp_rw : Eq (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ p₁ -ᵥ x) '' {p₁, p₂})) (k ∙ (p₁ -ᵥ p₂))
Tactic: simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
    Submodule.span_insert_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
simp_rw : Eq (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ p₁ -ᵥ x) '' {p₁, p₂})) (k ∙ (p₁ -ᵥ p₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₁ -ᵥ p₂))
have simp_rw₁ : Eq (α := Submodule k V) (Submodule.span k {p₁ -ᵥ p₁, p₁ -ᵥ p₂}) (k ∙ (p₁ -ᵥ p₂))
Tactic: simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
    Submodule.span_insert_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
simp_rw : Eq (α := Submodule k V) (Submodule.span k ((fun (x : P) ↦ p₁ -ᵥ x) '' {p₁, p₂})) (k ∙ (p₁ -ᵥ p₂))
simp_rw₁ : Eq (α := Submodule k V) (Submodule.span k {p₁ -ᵥ p₁, p₁ -ᵥ p₂}) (k ∙ (p₁ -ᵥ p₂))
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₁ -ᵥ p₂))
have simp_rw₂ : Eq (α := Submodule k V) (Submodule.span k {0, p₁ -ᵥ p₂}) (k ∙ (p₁ -ᵥ p₂))
Tactic: simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
    Submodule.span_insert_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₂ -ᵥ p₁))
have rw : Eq (α := Submodule k V) (vectorSpan k (P := P) {p₂, p₁}) (k ∙ (p₂ -ᵥ p₁))
Tactic: rw [pair_comm, vectorSpan_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
rw : Eq (α := Submodule k V) (vectorSpan k (P := P) {p₂, p₁}) (k ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₂ -ᵥ p₁))
have rw₁ : Eq (α := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (k ∙ (p₂ -ᵥ p₁))
Tactic: rw [pair_comm, vectorSpan_pair]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
have rw : Membership.mem (γ := Submodule k V) (k ∙ (p₁ -ᵥ p₂)) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
Tactic: rw [vectorSpan_pair, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (k ∙ (p₁ -ᵥ p₂)) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
have rw₁ : (∃ (a : k), a • (p₁ -ᵥ p₂) = v) ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
Tactic: rw [vectorSpan_pair, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
have rw : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
Tactic: rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
have rw₁ : (∃ (a : k), a • (p₂ -ᵥ p₁) = v) ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
Tactic: rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₁) ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
have rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {p₁, p₂})) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {p₁, p₂})) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₁) ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
have rw₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic (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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (direction (P := P) (affineSpan k {p₁, p₂})) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
rw₁ : Membership.mem (γ := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (v +ᵥ p₁) ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
have rw₂ : (∃ (r : k), r • (p₂ -ᵥ p₁) = v) ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
Tactic: rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]