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
ι : Type u_4
p : ι → P
i₀ : ι
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₀))
⊢ 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_right_ne k _ (Set.mem_univ i₀)]

Premises used: Set.image_univ, vectorSpan_image_eq_span_vsub_set_right_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) ↦ x -ᵥ p i₀) '' 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) ↦ x -ᵥ p i₀) '' 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) ∧ x -ᵥ p i₀ = v) ↔
    ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = 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:
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) ∧ x -ᵥ p i₀ = v) →
    ∃ (a : ι) (_ : a ≠ i₀), p a -ᵥ p i₀ = v
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
⊢ (∃ (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
-- 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 a -ᵥ p i₀ = 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 a -ᵥ p i₀ = 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 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:
fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩

Premises used: Set.univ, _private.0.vectorSpan_range_eq_span_range_vsub_right_ne.match_1, Membership.mem, Exists, VSub.vsub, And, And.intro, Exists.intro, Set.mem_univ, Eq, Not, rfl
-- 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 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:
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, 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
A : Set P
inst_4 : Nonempty.{u_3 + 1} (↑A : Type u_3)
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))
⊢ Eq (α := 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]

Premises used: eq_top_iff
-- 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
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)

Tactic:
affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx

Premises used: affineSpan_induction'
-- 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
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 ⋯)
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) ⋯)
⊢ 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)

Tactic:
refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
-- 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
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
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 ⋯)

Tactic:
subset_affineSpan _ _ hy

Premises used: subset_affineSpan
-- 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
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
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 ⋯)

Tactic:
exact subset_affineSpan _ _ hy

Premises used: subset_affineSpan
-- 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
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
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) ⋯)

Tactic:
AffineSubspace.smul_vsub_vadd_mem _ _

Premises used: Set.Mem, AffineSubspace.smul_vsub_vadd_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
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
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) ⋯)

Tactic:
exact AffineSubspace.smul_vsub_vadd_mem _ _

Premises used: AffineSubspace.smul_vsub_vadd_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 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)) ⊤

Tactic:
ext_of_direction_eq _
      ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩

Premises used: Set.mem_singleton, AffineSubspace.mem_top, mem_affineSpan, And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq, Set.mem_union_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 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)))) ⊤
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) ⊤)
⊢ Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)) ⊤

Tactic:
convert!
    ext_of_direction_eq _
      ⟨p, mem_affineSpan k (Set.mem_union_left _ (Set.mem_singleton _)), mem_top k V p⟩

Premises used: Set.mem_singleton, AffineSubspace.mem_top, mem_affineSpan, And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq, Set.mem_union_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 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)))) ⊤
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)))
⊢ 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:
rw [direction_affineSpan, direction_top,
    vectorSpan_eq_span_vsub_set_right k (Set.mem_union_left _ (Set.mem_singleton _) : p ∈ _),
    eq_top_iff, ← h]

Premises used: Set.mem_singleton, direction_affineSpan, eq_top_iff, AffineSubspace.direction_top, Set.mem_union_left, 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 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)))) ⊤
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))
⊢ 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:
apply Submodule.span_mono

Premises used: 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 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 }
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)
⊢ Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s)) (↑v' : V)

Tactic:
use (v' : V) +ᵥ p

Premises used: Subtype.val
-- 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 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 P) ({p} ∪ (fun (v : V) ↦ v +ᵥ p) '' s) ((↑v' : V) +ᵥ p) ∧
    (fun (x : P) ↦ x -ᵥ p) ((↑v' : V) +ᵥ p) = (↑v' : V)

Tactic:
simp
-- 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
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₂))
simp_rw₂ : Eq (α := Submodule k V) (Submodule.span k {0, p₁ -ᵥ p₂}) (k ∙ (p₁ -ᵥ p₂))
⊢ Eq (α := Submodule k V) (vectorSpan 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]

Premises used: Set.image_pair, vectorSpan_eq_span_vsub_set_left, Set.mem_insert, vsub_self, Submodule.span_insert_zero
-- 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
p₁ p₂ : P
rw : Eq (α := Submodule k V) (vectorSpan k (P := P) {p₂, p₁}) (k ∙ (p₂ -ᵥ p₁))
rw₁ rw₂ : Eq (α := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) (k ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule k V) (vectorSpan k (P := P) {p₁, p₂}) (k ∙ (p₂ -ᵥ p₁))

Tactic:
rw [pair_comm, vectorSpan_pair]

Premises used: vectorSpan_pair, Set.pair_comm
-- 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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (k ∙ (p₁ -ᵥ p₂)) v ↔ ∃ (r : k), r • (p₁ -ᵥ p₂) = v
rw₁ rw₂ : (∃ (a : k), a • (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

Tactic:
rw [vectorSpan_pair, Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, vectorSpan_pair
-- 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
p₁ p₂ : P
v : V
rw : Membership.mem (γ := Submodule k V) (k ∙ (p₂ -ᵥ p₁)) v ↔ ∃ (r : k), r • (p₂ -ᵥ p₁) = v
rw₁ rw₂ : (∃ (a : k), a • (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

Tactic:
rw [vectorSpan_pair_rev, Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton, vectorSpan_pair_rev
-- 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
r : k
p₁ p₂ : P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) ((lineMap p₁ p₂ : (a : k) → P) r : P)

Tactic:
AffineMap.lineMap_mem _ (left_mem_affineSpan_pair _ _ _) (right_mem_affineSpan_pair _ _ _)

Premises used: AffineMap.lineMap_mem, right_mem_affineSpan_pair, left_mem_affineSpan_pair
-- 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
r : k
p₁ p₂ : P
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) ((lineMap p₂ p₁ : (a : k) → P) r : P)

Tactic:
AffineMap.lineMap_mem _ (right_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _)

Premises used: AffineMap.lineMap_mem, right_mem_affineSpan_pair, left_mem_affineSpan_pair
-- 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
r : k
p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (r • (p₂ -ᵥ p₁) +ᵥ p₁)

Tactic:
AffineMap.lineMap_mem_affineSpan_pair _ _ _

Premises used: Set.Mem, AffineMap.lineMap_mem_affineSpan_pair
-- 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
r : k
p₁ p₂ : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {p₁, p₂}) (r • (p₁ -ᵥ p₂) +ᵥ p₂)

Tactic:
AffineMap.lineMap_rev_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_rev_mem_affineSpan_pair, Set.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
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
rw₂ rw₃ : (∃ (r : k), r • (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

Tactic:
rw [vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _), direction_affineSpan,
    mem_vectorSpan_pair_rev]

Premises used: direction_affineSpan, mem_vectorSpan_pair_rev, left_mem_affineSpan_pair, AffineSubspace.vadd_mem_iff_mem_direction