awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
x : V
h :
  (∃ (x_1 : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) x_1 ∧ ∃ y ∈ s, x_1 + y = x) ↔
    ∃ p₁ ∈ s, ∃ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v ∧ x = v + p₁
⊢ x ∈ (↑(vectorSpan k s) : Set V) + s ↔ x ∈ (↑(affineSpan k s) : Set V)

Tactic:
simp [mem_add, spanPoints]

Premises used: spanPoints, Set.mem_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
x : V
⊢ (∃ (x_1 : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) x_1 ∧ ∃ y ∈ s, x_1 + y = x) ↔
    ∃ p₁ ∈ s, ∃ (v : V), Membership.mem (γ := Submodule k V) (vectorSpan k s) v ∧ x = v + p₁

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
v : V
hp : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
hv : Membership.mem (γ := Submodule k V) (vectorSpan k s) v
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k s) (v +ᵥ p)

Tactic:
vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan k hp hv

Premises used: vadd_mem_spanPoints_of_mem_spanPoints_of_mem_vectorSpan, Set.Mem, setOf, spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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₂ : P
hp₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p₁
hp₂ : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p₂
⊢ Membership.mem (γ := Submodule k V) (vectorSpan k s) (p₁ -ᵥ p₂)

Tactic:
vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints k hp₁ hp₂

Premises used: vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
s₁ : AffineSubspace k P
h : s ⊆ (↑s₁ : Set P)
⊢ affineSpan k s ≤ s₁

Tactic:
AffineSubspace.spanPoints_subset_coe_of_subset_coe h

Premises used: AffineSubspace.spanPoints_subset_coe_of_subset_coe, Set.Mem, setOf, spanPoints, Set.Subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₁
hp₂ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₂
hp₃ : Membership.mem (γ := Set P) (⋂ s' ∈ s, (↑s' : Set P)) p₃
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
rw :
  ∀ (hp₁ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₁ ∈ (↑i : Set P))
    (hp₂ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₂ ∈ (↑i : Set P))
    (hp₃ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₃ ∈ (↑i : Set P)) (s₂ : AffineSubspace k P) (hs₂ : s₂ ∈ s),
    c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)

Tactic:
rw [Set.mem_iInter₂] at *

Premises used: Set.mem_iInter₂
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₁ ∈ (↑i : Set P)
hp₂ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₂ ∈ (↑i : Set P)
hp₃ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₃ ∈ (↑i : Set P)
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)

Tactic:
s₂.smul_vsub_vadd_mem c (hp₁ s₂ hs₂) (hp₂ s₂ hs₂) (hp₃ s₂ hs₂)

Premises used: Set.Mem, AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₁ ∈ (↑i : Set P)
hp₂ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₂ ∈ (↑i : Set P)
hp₃ : ∀ (i : AffineSubspace k P) (j : i ∈ s), p₃ ∈ (↑i : Set P)
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ (↑s₂ : Set P)

Tactic:
exact s₂.smul_vsub_vadd_mem c (hp₁ s₂ hs₂) (hp₂ s₂ hs₂) (hp₃ s₂ hs₂)

Premises used: AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ≤ s₂ ↔ (↑s₁ : Set P) ⊆ (↑s₂ : Set P)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ≤ s₂ ↔ ∀ p ∈ s₁, p ∈ s₂

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ < s₂ ↔ (↑s₁ : Set P) ⊂ (↑s₂ : Set P)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ ¬s₁ ≤ s₂ ↔ ∃ p ∈ s₁, p ∉ s₂

Tactic:
Set.not_subset

Premises used: Set.Subset, Set.not_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ < s₂
⊢ ∃ p ∈ s₂, p ∉ s₁

Tactic:
Set.exists_of_ssubset h

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
rw : s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
rw₁ rw₂ : (s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
⊢ s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Tactic:
rw [lt_iff_le_not_ge, not_le_iff_exists]

Premises used: lt_iff_le_not_ge, AffineSubspace.not_le_iff_exists
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ : Set P).Nonempty
hle : s₁ ≤ s₂
⊢ s₁ = s₂

Tactic:
let ⟨p, hp⟩ := hn
  ext_of_direction_eq hd ⟨p, hp, hle hp⟩

Premises used: And.intro, Exists.intro, AffineSubspace.ext_of_direction_eq, _private.0.AffineSubspace.eq_of_direction_eq_of_nonempty_of_le.match_1, Eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
s₁ s₂ : AffineSubspace k P
inst_3 : Nonempty.{u_3 + 1} ↥s₁
⊢ Nonempty.{u_3 + 1} ↥(s₁ ⊔ s₂)

Tactic:
.map (Set.inclusion <| SetLike.le_def.1 le_sup_left) ‹_›

Premises used: le_sup_left, SetLike.le_def, Iff.mp, Set.inclusion, Nonempty.map
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
s₁ s₂ : AffineSubspace k P
inst_3 : Nonempty.{u_3 + 1} ↥s₂
⊢ Nonempty.{u_3 + 1} ↥(s₁ ⊔ s₂)

Tactic:
.map (Set.inclusion <| SetLike.le_def.1 le_sup_right) ‹_›

Premises used: SetLike.le_def, le_sup_right, Iff.mp, Set.inclusion, Nonempty.map
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) (sInf {s' : AffineSubspace k P | s ⊆ (↑s' : Set P)})

Tactic:
le_antisymm (affineSpan_le_of_subset_coe <| Set.subset_iInter₂ fun _ => id)
    (sInf_le (subset_spanPoints k _))

Premises used: Set.subset_iInter₂, id, le_antisymm, affineSpan_le_of_subset_coe, sInf_le, subset_spanPoints
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
⊢ Eq.{u_3 + 1} (α := AffineSubspace k P) (affineSpan k ∅) ⊥

Tactic:
(AffineSubspace.gi k V P).gc.l_bot

Premises used: AffineSubspace.gi, GaloisConnection.l_bot, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
⊢ Eq.{u_3 + 1} (α := AffineSubspace k P) (affineSpan k univ) ⊤

Tactic:
eq_top_iff.2 <| subset_affineSpan k _

Premises used: Iff.mpr, eq_top_iff, subset_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
Q : AffineSubspace k P
⊢ affineSpan k s ≤ Q ↔ s ⊆ (↑Q : Set P)

Tactic:
(AffineSubspace.gi k V P).gc _ _

Premises used: AffineSubspace.gi, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s t : Set P
⊢ Eq (α := AffineSubspace k P) (affineSpan k (s ∪ t)) (affineSpan k s ⊔ affineSpan k t)

Tactic:
(AffineSubspace.gi k V P).gc.l_sup

Premises used: AffineSubspace.gi, GaloisConnection.l_sup, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Type u_5
s : ι → Set P
⊢ Eq.{u_3 + 1} (α := AffineSubspace k P) (affineSpan k (⋃ (i : ι), s i)) (⨆ (i : ι), affineSpan k (s i))

Tactic:
(AffineSubspace.gi k V P).gc.l_iSup

Premises used: GaloisConnection.l_iSup, AffineSubspace.gi, Set.iUnion, GaloisInsertion.gc
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
⊢ (↑⊤ : Set P) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
⊢ Membership.mem (γ := AffineSubspace k P) ⊤ p

Tactic:
Set.mem_univ p

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
h : ∀ (x : P), Membership.mem (γ := AffineSubspace k P) (mk' p ⊤) x ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x
⊢ Eq (α := AffineSubspace k P) (mk' p ⊤) ⊤

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p x : P
⊢ Membership.mem (γ := AffineSubspace k P) (mk' p ⊤) x ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x

Tactic:
simp [mem_mk']

Premises used: AffineSubspace.mem_mk'
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
obtain : ∀ (p : P), Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤

Tactic:
obtain ⟨p⟩ := S.nonempty

Premises used: AddTorsor.nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
h :
  ∀ (v : V),
    Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v ↔
      Membership.mem (γ := Submodule k V) ⊤ v
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
v : V
⊢ Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v ↔ Membership.mem (γ := Submodule k V) ⊤ v

Tactic:
⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩

Premises used: imp_intro, Iff.intro, Submodule.mem_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
v : V
h :
  ∀ (_hv : Membership.mem (γ := Submodule k V) ⊤ v),
    Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v
⊢ Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v ↔ Membership.mem (γ := Submodule k V) ⊤ v

Tactic:
refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
v : V
_hv : Membership.mem (γ := Submodule k V) ⊤ v
⊢ Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ((v +ᵥ p) -ᵥ p)

Tactic:
have hpv : ((v +ᵥ p) -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
    vsub_mem_direction (mem_top k V _) (mem_top k V _)
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
p : P
v : V
_hv : Membership.mem (γ := Submodule k V) ⊤ v
hpv : Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ((v +ᵥ p) -ᵥ p)
h h₁ h₂ h₃ :
  ∀ (hpv : Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v),
    Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v
⊢ Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v

Tactic:
rwa [vadd_vsub] at hpv

Premises used: vadd_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
⊢ (↑⊥ : Set P) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
contra : Eq.{u_3 + 1} (α := AffineSubspace k P) ⊥ ⊤
⊢ Eq.{u_3 + 1} (α := Set P) ∅ univ

Tactic:
rw [AffineSubspace.ext_iff, bot_coe, top_coe] at contra

Premises used: AffineSubspace.bot_coe, AffineSubspace.ext_iff, AffineSubspace.top_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
contra : Eq.{u_3 + 1} (α := Set P) ∅ univ
⊢ False

Tactic:
Set.empty_ne_univ contra

Premises used: Set.empty_ne_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
contra : Eq.{u_3 + 1} (α := Set P) ∅ univ
⊢ False

Tactic:
exact Set.empty_ne_univ contra

Premises used: Set.empty_ne_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
ι : Sort u_4
p₁ p₂ : P
⊢ Nontrivial.{u_3} (AffineSubspace k P)

Tactic:
⟨⟨⊥, ⊤, bot_ne_top k V P⟩⟩

Premises used: Bot.bot, Nontrivial.mk, Exists.intro, AffineSubspace.bot_ne_top, Top.top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
h : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
rw : s ≠ ∅
⊢ s.Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
h : Eq.{u_3 + 1} (α := AffineSubspace k P) (affineSpan k ∅) ⊤
⊢ Eq.{u_3 + 1} (α := AffineSubspace k P) ⊥ ⊤

Tactic:
rw [AffineSubspace.span_empty] at h

Premises used: AffineSubspace.span_empty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
h : Eq.{u_3 + 1} (α := AffineSubspace k P) ⊥ ⊤
⊢ False

Tactic:
bot_ne_top k V P h

Premises used: AffineSubspace.bot_ne_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
h : Eq.{u_3 + 1} (α := AffineSubspace k P) ⊥ ⊤
⊢ False

Tactic:
exact bot_ne_top k V P h

Premises used: AffineSubspace.bot_ne_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
h : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
rw : Eq (α := Submodule k V) (direction (affineSpan k s)) ⊤
rw₁ : Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule k V) ⊤ ⊤
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
rw [← direction_affineSpan, h, direction_top]

Premises used: direction_affineSpan, AffineSubspace.direction_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩

Premises used: Iff.intro, AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
refine : Eq (α := Submodule k V) (vectorSpan k s) ⊤ → Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
refine ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
this : Nonempty.{u_3 + 1} ↥(affineSpan k s)
obtain :
  ∀ (p : P) (hp : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p),
    Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤

Tactic:
obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this

Premises used: affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
p : P
hp : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p
rw : Eq (α := Submodule k V) (direction (affineSpan k s)) (direction.{u_1, u_2, u_3} (P := P) ⊤)
rw₁ : Eq (α := Submodule k V) (vectorSpan k s) (direction.{u_1, u_2, u_3} (P := P) ⊤)
rw₂ : Eq (α := Submodule k V) ⊤ (direction.{u_1, u_2, u_3} (P := P) ⊤)
rw₃ rw₄ : Eq.{u_2 + 1} (α := Submodule k V) ⊤ ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤

Tactic:
rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]

Premises used: direction_affineSpan, AffineSubspace.mem_top, AffineSubspace.eq_iff_direction_eq_of_mem, AffineSubspace.direction_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
suffices : Nonempty.{u_3 + 1} ↥(affineSpan k s)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤

Tactic:
suffices Nonempty (affineSpan k s) by
    obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
    rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
obtain : ∀ (x : P) (hx : x ∈ s), Nonempty.{u_3 + 1} ↥(affineSpan k s)
⊢ Nonempty.{u_3 + 1} ↥(affineSpan k s)

Tactic:
obtain ⟨x, hx⟩ := hs
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
x : P
hx : x ∈ s
⊢ Nonempty.{u_3 + 1} ↥(affineSpan k s)

Tactic:
⟨⟨x, mem_affineSpan k hx⟩⟩

Premises used: mem_affineSpan, Nonempty.intro, Subtype.mk
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
x : P
hx : x ∈ s
⊢ Nonempty.{u_3 + 1} ↥(affineSpan k s)

Tactic:
exact ⟨⟨x, mem_affineSpan k hx⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
inst_3 : Nontrivial P
inl : ∀ (hs : s = ∅), Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
inr : ∀ (hs : s.Nonempty), Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
inst_3 : Nontrivial P
hs : s = ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]

Premises used: AddTorsor.subsingleton_iff, not_subsingleton, subsingleton_iff_bot_eq_top
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
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
S : AffineSpace V P
s : Set P
inst_3 : Nontrivial P
hs : s.Nonempty
inr inr₁ : Eq (α := Submodule k V) (vectorSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤

Tactic:
rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]

Premises used: AffineSubspace.affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty