awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ LE.le (α := Submodule k V)
    (Submodule.span k ((↑s₁ : Set P) -ᵥ (↑s₁ : Set P)) ⊔ Submodule.span k ((↑s₂ : Set P) -ᵥ (↑s₂ : Set P)))
    (Submodule.span k ((↑(s₁ ⊔ s₂) : Set P) -ᵥ (↑(s₁ ⊔ s₂) : Set P)))

Tactic:
exact
    sup_le
      (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_left : s₁ ≤ s₁ ⊔ s₂)) hp)
      (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_right : s₂ ≤ s₁ ⊔ s₂)) hp)

Premises used: sup_le
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
obtain : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
obtain ⟨p₁, hp₁⟩ := h1
-- 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
h2 : (↑s₂ : Set P).Nonempty
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
obtain : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
obtain ⟨p₂, hp₂⟩ := h2
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
rw : s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction ∧ ∃ x ∈ (s₁ ⊔ s₂).direction, x ∉ s₁.direction ⊔ s₂.direction
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
rw [SetLike.lt_iff_le_and_exists]

Premises used: SetLike.lt_iff_le_and_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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
right : p₂ -ᵥ p₁ ∉ s₁.direction ⊔ s₂.direction
⊢ s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction ∧ ∃ x ∈ (s₁ ⊔ s₂).direction, x ∉ s₁.direction ⊔ s₂.direction

Tactic:
use sup_direction_le s₁ s₂, p₂ -ᵥ p₁,
    vsub_mem_direction ((le_sup_right : s₂ ≤ s₁ ⊔ s₂) hp₂) ((le_sup_left : s₁ ≤ s₁ ⊔ s₂) hp₁)

Premises used: le_sup_left, AffineSubspace.vsub_mem_direction, le_sup_right, AffineSubspace.sup_direction_le
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
h : p₂ -ᵥ p₁ ∈ s₁.direction ⊔ s₂.direction
⊢ ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction, y + z = p₂ -ᵥ p₁

Tactic:
rw [Submodule.mem_sup] at h

Premises used: Submodule.mem_sup
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
h : ∃ y ∈ s₁.direction, ∃ z ∈ s₂.direction, y + z = p₂ -ᵥ p₁
right : ∀ (v₁ : V) (hv₁ : v₁ ∈ s₁.direction) (v₂ : V) (hv₂ : v₂ ∈ s₂.direction) (hv₁v₂ : v₁ + v₂ = p₂ -ᵥ p₁), False
⊢ False

Tactic:
rcases h with ⟨v₁, hv₁, v₂, hv₂, hv₁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
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ + v₂ = p₂ -ᵥ p₁
⊢ v₁ +ᵥ p₁ = -v₂ +ᵥ p₂

Tactic:
rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v₁, add_assoc, ←
    vadd_vsub_assoc, ← neg_neg v₂, add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub,
    vsub_eq_zero_iff_eq] at hv₁v₂

Premises used: vadd_vsub_assoc, sub_eq_zero, vsub_vadd_eq_vsub_sub, add_assoc, vsub_eq_zero_iff_eq, sub_eq_add_neg, neg_neg, add_comm, neg_vsub_eq_vsub_rev
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ False

Tactic:
Set.Nonempty.ne_empty ?_ he

Premises used: Set.Nonempty.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
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
right : ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
⊢ False

Tactic:
refine Set.Nonempty.ne_empty ?_ he

Premises used: Set.Nonempty.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
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
right : v₁ +ᵥ p₁ ∈ (↑s₂ : Set P)
⊢ ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty

Tactic:
use v₁ +ᵥ p₁, vadd_mem_of_mem_direction hv₁ hp₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
right : -v₂ +ᵥ p₂ ∈ (↑s₂ : Set P)
⊢ v₁ +ᵥ p₁ ∈ (↑s₂ : Set P)

Tactic:
rw [hv₁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
s₁ s₂ : AffineSubspace k P
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ -v₂ +ᵥ p₂ ∈ (↑s₂ : Set P)

Tactic:
vadd_mem_of_mem_direction (Submodule.neg_mem _ hv₂) hp₂

Premises used: Set.Mem, Submodule.neg_mem, AffineSubspace.vadd_mem_of_mem_direction
-- 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
he : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ -v₂ +ᵥ p₂ ∈ (↑s₂ : Set P)

Tactic:
exact vadd_mem_of_mem_direction (Submodule.neg_mem _ hv₂) hp₂

Premises used: Submodule.neg_mem, AffineSubspace.vadd_mem_of_mem_direction
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
by_contra : ∀ (h : ¬((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty), False
⊢ ((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty

Tactic:
by_contra h
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ¬((↑s₁ : Set P) ∩ (↑s₂ : Set P)).Nonempty
⊢ (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at h

Premises used: Set.not_nonempty_iff_eq_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
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
⊢ s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Tactic:
have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
hlt : s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction
⊢ ⊤ < (s₁ ⊔ s₂).direction

Tactic:
rw [hd] at hlt
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
hlt : ⊤ < (s₁ ⊔ s₂).direction
⊢ False

Tactic:
not_top_lt hlt

Premises used: not_top_lt
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = ∅
hlt : ⊤ < (s₁ ⊔ s₂).direction
⊢ False

Tactic:
exact not_top_lt hlt

Premises used: not_top_lt
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
obtain : ∀ (p : P) (hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)), ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
⊢ ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}

Tactic:
obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top

Premises used: IsCompl.sup_eq_top, AffineSubspace.inter_nonempty_of_nonempty_of_sup_direction_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₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
h : (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}
⊢ ∃ (p : P), (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}

Tactic:
use 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₁ s₂ : AffineSubspace k P
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
h : ∀ (q : P), q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) ↔ Membership.mem (γ := Set P) {p} q
⊢ (↑s₁ : Set P) ∩ (↑s₂ : Set P) = {p}

Tactic:
ext q
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
h : q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) → q = p
h₁ : q = p → q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
⊢ q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P) ↔ q = p

Tactic:
constructor
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
⊢ q -ᵥ p ∈ s₁.direction ⊓ s₂.direction

Tactic:
have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction :=
      ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
hq1 : q ∈ (↑s₁ : Set P)
hq2 : q ∈ (↑s₂ : Set P)
hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction
h : ∀ (hqp : Membership.mem (γ := Submodule k V) ⊥ (q -ᵥ p)), q = p
h₁ : ∀ (hqp : q -ᵥ p = 0), q = p
h₂ h₃ h₄ h₅ : ∀ (hqp : q = p), q = p
⊢ q = p

Tactic:
rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp

Premises used: Submodule.mem_bot, vsub_eq_zero_iff_eq, IsCompl.inf_eq_bot
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
⊢ q = p → q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)

Tactic:
fun h => h.symm ▸ hp

Premises used: Eq.rec, Eq.symm
-- 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
h1 : (↑s₁ : Set P).Nonempty
h2 : (↑s₂ : Set P).Nonempty
hd : IsCompl s₁.direction s₂.direction
p : P
hp : p ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)
q : P
⊢ q = p → q ∈ (↑s₁ : Set P) ∩ (↑s₂ : Set P)

Tactic:
exact fun h => h.symm ▸ hp
-- 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 : AffineSubspace k P
⊢ affineSpan k (↑s : Set P) = s

Tactic:
le_antisymm ?_ (subset_affineSpan _ _)

Premises used: le_antisymm, 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 : AffineSubspace k P
refine : affineSpan k (↑s : Set P) ≤ s
⊢ affineSpan k (↑s : Set P) = s

Tactic:
refine le_antisymm ?_ (subset_affineSpan _ _)

Premises used: le_antisymm, 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k (↑s : Set P)) v
⊢ v +ᵥ p₁ ∈ s

Tactic:
vadd_mem_of_mem_direction hv hp₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ (↑s : Set P)
v : V
hv : Membership.mem (γ := Submodule k V) (vectorSpan k (↑s : Set P)) v
⊢ v +ᵥ p₁ ∈ s

Tactic:
exact vadd_mem_of_mem_direction hv hp₁

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- 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
d₁ d₂ : Submodule k V
simp_rw : (∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) ↔ ∀ ⦃x : V⦄, x ∈ d₁ → x ∈ d₂
⊢ LE.le (α := AffineSubspace k P) (mk' p d₁) (mk' p d₂) ↔ d₁ ≤ d₂

Tactic:
simp_rw [SetLike.le_def, mem_mk']

Premises used: SetLike.le_def, 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
p : P
d₁ d₂ : Submodule k V
⊢ (∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) ↔ ∀ ⦃x : V⦄, x ∈ d₁ → x ∈ d₂

Tactic:
⟨fun h x hx ↦ ?_, fun h x hx ↦ h hx⟩

Premises used: Iff.intro
-- 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
d₁ d₂ : Submodule k V
refine : ∀ (h : ∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) (x : V) (hx : x ∈ d₁), x ∈ d₂
⊢ (∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂) ↔ ∀ ⦃x : V⦄, x ∈ d₁ → x ∈ d₂

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ h 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
p : P
d₁ d₂ : Submodule k V
h : ∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂
x : V
hx : x ∈ d₁
⊢ (x +ᵥ p) -ᵥ p ∈ d₁

Tactic:
simpa using 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
p : P
d₁ d₂ : Submodule k V
h : ∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂
x : V
hx : x ∈ d₁
⊢ x ∈ d₂

Tactic:
simpa using h (show (x +ᵥ p) -ᵥ p ∈ d₁ by simpa using 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
p : P
⊢ StrictMono (α := Submodule k V) (β := AffineSubspace k P) (mk' p)

Tactic:
strictMono_of_le_iff_le (fun _ _ ↦ (mk'_le_mk'_iff p).symm)

Premises used: AffineSubspace.mk'_le_mk'_iff, strictMono_of_le_iff_le, Iff.symm
-- 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
⊢ (↑(affineSpan k s) : Set P).Nonempty ↔ s.Nonempty

Tactic:
spanPoints_nonempty k s

Premises used: setOf, spanPoints_nonempty, 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
ι : Type u_4
s : Set P
inst_4 : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ Nonempty.{u_3 + 1} ↥(affineSpan k s)

Tactic:
((nonempty_coe_sort.1 ‹_›).affineSpan _).to_subtype

Premises used: Set.nonempty_coe_sort, Set.Nonempty.to_subtype, Iff.mp, Set.Nonempty.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
inst_3 : AffineSpace V P
s : Set P
rw : ¬Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
rw₁ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ ¬s = ∅
rw₂ : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅
rw₃ : (↑(affineSpan k s) : Set P).Nonempty ↔ s ≠ ∅
rw₄ : s.Nonempty ↔ s ≠ ∅
rw₅ rw₆ : s ≠ ∅ ↔ s ≠ ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    nonempty_iff_ne_empty]

Premises used: not_iff_not, Ne, affineSpan_nonempty, Set.nonempty_iff_ne_empty, AffineSubspace.nonempty_iff_ne_bot
-- 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
rw : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅
⊢ LT.lt (α := AffineSubspace k P) ⊥ (affineSpan k s) ↔ s.Nonempty

Tactic:
rw [bot_lt_iff_ne_bot, nonempty_iff_ne_empty]

Premises used: bot_lt_iff_ne_bot, 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
inst_3 : AffineSpace V P
s : Set P
⊢ Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅

Tactic:
(affineSpan_eq_bot _).not

Premises used: Iff.not, affineSpan_eq_bot
-- 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
⊢ Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅

Tactic:
exact (affineSpan_eq_bot _).not

Premises used: Iff.not, affineSpan_eq_bot
-- 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
inst_4 : Subsingleton P
rw : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ LT.lt (α := AffineSubspace k P) ⊥ (affineSpan k s)
rw₁ rw₂ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ s.Nonempty

Tactic:
rw [← bot_lt_affineSpan k, IsSimpleOrder.bot_lt_iff_eq_top]

Premises used: bot_lt_affineSpan, IsSimpleOrder.bot_lt_iff_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
inst_3 : AffineSpace V P
x : P
s : Set P
p : P → Prop
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
mem : ∀ x ∈ s, p x
smul_vsub_vadd : ∀ (c : k) (u v w : P), p u → p v → p w → p (c • (u -ᵥ v) +ᵥ w)
⊢ p x

Tactic:
(affineSpan_le (Q := ⟨{x | p x}, smul_vsub_vadd⟩)).mpr mem h

Premises used: Iff.mpr, Set.Mem, setOf, affineSpan_le
-- 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 : (x : P) → Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u) (v : P)
    (hv : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v) (w : P)
    (hw : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x
suffices : ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
⊢ p x h

Tactic:
suffices ∃ (hx : x ∈ affineSpan k s), p x hx from this.elim fun hx hc ↦ hc