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
ι : Type u_5
inst_3 : Fintype ι
p : ι → P
h : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
obtain : ∀ (i : ι), 0 < Fintype.card ι
⊢ 0 < Fintype.card ι

Tactic:
obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h

Premises used: AffineSubspace.nonempty_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
ι : Type u_5
inst_3 : Fintype ι
p : ι → P
h : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
i : ι
⊢ 0 < Fintype.card ι

Tactic:
Fintype.card_pos_iff.mpr ⟨i⟩

Premises used: Iff.mpr, Nonempty.intro, Fintype.card_pos_iff
-- 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
inst_3 : Fintype ι
p : ι → P
h : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
i : ι
⊢ 0 < Fintype.card ι

Tactic:
exact Fintype.card_pos_iff.mpr ⟨i⟩

Premises used: Iff.mpr, Nonempty.intro, Fintype.card_pos_iff
-- 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
⊢ Nonempty.{u_3 + 1} ↥⊤

Tactic:
inferInstanceAs (Nonempty (⊤ : Set P))

Premises used: _private.0.AffineSubspace.instNonemptySubtypeMemTop._proof_1
-- 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
⊢ p ∉ ⊥

Tactic:
Set.notMem_empty p

Premises used: Set.Mem, Set.notMem_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
ι : Sort u_4
p₁ p₂ : P
⊢ IsEmpty.{u_3 + 1} ↥⊥

Tactic:
Subtype.isEmpty_of_false fun _ ↦ notMem_bot _ _ _

Premises used: Subtype.isEmpty_of_false, AffineSubspace.notMem_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
rw : Eq (α := Submodule k V) (vectorSpan k (↑⊥ : Set P)) ⊥
rw₁ : Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
rw₂ : Eq (α := Submodule k V) (Submodule.span k (VSub.vsub.{u_2, u_3} (P := Set P) ∅ ∅)) ⊥
rw₃ : Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ∅) ⊥
rw₄ rw₅ : Eq.{u_2 + 1} (α := Submodule k V) ⊥ ⊥
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥

Tactic:
rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]

Premises used: AffineSubspace.bot_coe, AffineSubspace.direction_eq_vectorSpan, Set.vsub_empty, vectorSpan_def, Submodule.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
Q : AffineSubspace k P
⊢ (↑Q : Set P) = ∅ ↔ Q = ⊥

Tactic:
coe_injective.eq_iff' (bot_coe _ _ _)

Premises used: AffineSubspace.bot_coe, Function.Injective.eq_iff', AffineSubspace.coe_injective
-- 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
Q : AffineSubspace k P
⊢ (↑Q : Set P) = univ ↔ Q = ⊤

Tactic:
coe_injective.eq_iff' (top_coe _ _ _)

Premises used: Function.Injective.eq_iff', AffineSubspace.top_coe, AffineSubspace.coe_injective
-- 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
Q : AffineSubspace k P
rw : (↑Q : Set P) ≠ ∅ ↔ Q ≠ ⊥
⊢ (↑Q : Set P).Nonempty ↔ Q ≠ ⊥

Tactic:
rw [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
Q : AffineSubspace k P
⊢ (↑Q : Set P) ≠ ∅ ↔ Q ≠ ⊥

Tactic:
not_congr Q.coe_eq_bot_iff

Premises used: AffineSubspace.coe_eq_bot_iff, not_congr
-- 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
Q : AffineSubspace k P
⊢ (↑Q : Set P) ≠ ∅ ↔ Q ≠ ⊥

Tactic:
exact not_congr Q.coe_eq_bot_iff

Premises used: AffineSubspace.coe_eq_bot_iff, not_congr
-- 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
Q : AffineSubspace k P
rw : Q = ⊥ ∨ Q ≠ ⊥
⊢ Q = ⊥ ∨ (↑Q : Set P).Nonempty

Tactic:
rw [nonempty_iff_ne_bot]

Premises used: 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
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥

Tactic:
apply eq_or_ne

Premises used: eq_or_ne
-- 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
inst_3 : Subsingleton P
s : AffineSubspace k P
rw : (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
⊢ s = ⊥ ∨ s = ⊤

Tactic:
rw [← coe_eq_bot_iff, ← coe_eq_univ_iff]

Premises used: AffineSubspace.coe_eq_univ_iff, AffineSubspace.coe_eq_bot_iff
-- 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
inst_3 : Subsingleton P
s : AffineSubspace k P
inl : ∀ (h : (↑s : Set P) = ∅), (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
inr : ∀ (h : (↑s : Set P).Nonempty), (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ

Tactic:
rcases (s : Set P).eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty, SetLike.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
ι : Sort u_4
p₁ p₂ : P
inst_3 : Subsingleton P
s : AffineSubspace k P
h : (↑s : Set P) = ∅
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ

Tactic:
.inl h

Premises used: Or.inl
-- 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
inst_3 : Subsingleton P
s : AffineSubspace k P
h : (↑s : Set P) = ∅
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ

Tactic:
exact .inl 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
ι : Sort u_4
p₁ p₂ : P
inst_3 : Subsingleton P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ

Tactic:
.inr h.eq_univ

Premises used: Set.Nonempty.eq_univ, Or.inr
-- 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
inst_3 : Subsingleton P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ

Tactic:
exact .inr h.eq_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
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
mp : s.direction = ⊤ → s = ⊤
mpr : s = ⊤ → s.direction = ⊤
⊢ s.direction = ⊤ ↔ s = ⊤

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 : AffineSubspace k P
h : (↑s : Set P).Nonempty
hd : s.direction = ⊤
⊢ s.direction = direction.{u_1, u_2, u_3} (P := P) ⊤

Tactic:
rw [← direction_top k V P] at hd

Premises used: 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 : AffineSubspace k P
h : (↑s : Set P).Nonempty
hd : s.direction = direction.{u_1, u_2, u_3} (P := P) ⊤
⊢ s = ⊤

Tactic:
ext_of_direction_eq hd ?_

Premises used: AffineSubspace.ext_of_direction_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
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
hd : s.direction = direction.{u_1, u_2, u_3} (P := P) ⊤
mp : ((↑s : Set P) ∩ (↑⊤ : Set P)).Nonempty
⊢ s = ⊤

Tactic:
refine ext_of_direction_eq hd ?_

Premises used: AffineSubspace.ext_of_direction_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
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
hd : s.direction = direction.{u_1, u_2, u_3} (P := P) ⊤
⊢ ((↑s : Set P) ∩ (↑⊤ : Set P)).Nonempty

Tactic:
simp [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
h : (↑⊤ : Set P).Nonempty
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤

Tactic:
simp
-- 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₁ : Set P) ⊓ (↑s₂ : Set P) = (↑s₁ : Set P) ∩ (↑s₂ : 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
p : P
s₁ s₂ : AffineSubspace k P
⊢ p ∈ s₁ ⊓ s₂ ↔ p ∈ s₁ ∧ p ∈ s₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- 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₁ ⊓ s₂) : Set P) -ᵥ (↑(s₁ ⊓ s₂) : Set P)))
    (Submodule.span k ((↑s₁ : Set P) -ᵥ (↑s₁ : Set P)) ⊓ Submodule.span k ((↑s₂ : Set P) -ᵥ (↑s₂ : Set P)))

Tactic:
le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_left) hp)
      (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_right) hp)

Premises used: trans, Set.Mem, sInf_le_sInf, Set.inter_subset_left, le_inf, Set.vsub_self_mono, Set.inter_subset_right
-- 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₁ ⊓ s₂) : Set P) -ᵥ (↑(s₁ ⊓ s₂) : Set P)))
    (Submodule.span k ((↑s₁ : Set P) -ᵥ (↑s₁ : Set P)) ⊓ Submodule.span k ((↑s₂ : Set P) -ᵥ (↑s₂ : Set P)))

Tactic:
exact
    le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_left) hp)
      (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_right) 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₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : ∀ (v : V), v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

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
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
h : v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ∧ v ∈ s₂.direction
h₃ : v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v ∈ s₂.direction
h₄ : v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
h₅ : v +ᵥ p ∈ s₁ ⊓ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
h₆ h₇ : v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction

Tactic:
rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

Premises used: Iff.mpr, Submodule.mem_inf, And.intro, AffineSubspace.vadd_mem_iff_mem_direction, AffineSubspace.mem_inf_iff
-- 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
p : P
h : p ∈ s₁ ⊓ s₂
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Tactic:
direction_inf_of_mem ((mem_inf_iff p s₁ s₂).1 h).1 ((mem_inf_iff p s₁ s₂).1 h).2

Premises used: AffineSubspace.direction_inf_of_mem, And.right, And.left, Iff.mp, AffineSubspace.mem_inf_iff
-- 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
t : Set (AffineSubspace k P)
⊢ (↑(sInf t) : Set P) = ⋂ s ∈ t, (↑s : Set P)

Tactic:
rfl

Premises used: iInf, Set.iInter, 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
t : Set (AffineSubspace k P)
⊢ p ∈ sInf t ↔ ∀ s ∈ t, p ∈ s

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, 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
t : Set (AffineSubspace k P)
⊢ LE.le (α := Submodule k V) (Submodule.span k ((↑(sInf t) : Set P) -ᵥ (↑(sInf t) : Set P)))
    (⨅ s ∈ t, Submodule.span k ((↑s : Set P) -ᵥ (↑s : Set P)))

Tactic:
le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

Premises used: Set.Mem, Set.biInter_subset_of_mem, le_iInf₂, Set.vsub_self_mono, Submodule.span_mono
-- 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
t : Set (AffineSubspace k P)
⊢ LE.le (α := Submodule k V) (Submodule.span k ((↑(sInf t) : Set P) -ᵥ (↑(sInf t) : Set P)))
    (⨅ s ∈ t, Submodule.span k ((↑s : Set P) -ᵥ (↑s : Set P)))

Tactic:
exact le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

Premises used: Set.biInter_subset_of_mem, le_iInf₂, Set.vsub_self_mono, Submodule.span_mono
-- 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
apply : ⨅ s ∈ t, s.direction ≤ (sInf t).direction
⊢ (sInf t).direction = ⨅ s ∈ t, s.direction

Tactic:
apply (direction_sInf t).antisymm

Premises used: LE.le.antisymm, AffineSubspace.direction_sInf
-- 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
rw : ∀ s ∈ t, v +ᵥ p ∈ s
⊢ v ∈ (sInf t).direction

Tactic:
rw [← vadd_mem_iff_mem_direction v ((mem_sInf_iff p t).mpr h), mem_sInf_iff]

Premises used: Iff.mpr, AffineSubspace.mem_sInf_iff, AffineSubspace.vadd_mem_iff_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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
s : AffineSubspace k P
hs : s ∈ t
rw : v ∈ s.direction
⊢ v +ᵥ p ∈ s

Tactic:
rw [vadd_mem_iff_mem_direction v (h s hs)]

Premises used: AffineSubspace.vadd_mem_iff_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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : Membership.mem (γ := Submodule k V) (⨅ s ∈ t, s.direction) v
s : AffineSubspace k P
hs : s ∈ t
⊢ ∀ (i : AffineSubspace k P) (i_1 : i ∈ t), v ∈ i.direction

Tactic:
simp only [Submodule.mem_iInf] at hv

Premises used: Submodule.mem_iInf
-- 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
s : AffineSubspace k P
hs : s ∈ t
hv : ∀ (i : AffineSubspace k P) (i_1 : i ∈ t), v ∈ i.direction
⊢ v ∈ s.direction

Tactic:
hv s 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
s : AffineSubspace k P
hs : s ∈ t
hv : ∀ (i : AffineSubspace k P) (i_1 : i ∈ t), v ∈ i.direction
⊢ v ∈ s.direction

Tactic:
exact hv s 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
t : Set (AffineSubspace k P)
p : P
h : p ∈ sInf t
⊢ (sInf t).direction = ⨅ s ∈ t, s.direction

Tactic:
direction_sInf_of_mem t p <| (mem_sInf_iff p t).mp h

Premises used: AffineSubspace.mem_sInf_iff, AffineSubspace.direction_sInf_of_mem, Iff.mp
-- 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 : ι → AffineSubspace k P
rw : (↑(sInf (range s)) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)
rw₁ : Eq.{u_3 + 1} (α := Set P) (⋂ s_1 ∈ range s, (↑s_1 : Set P)) (⋂ (i : ι), (↑(s i) : Set P))
rw₂ rw₃ : Eq.{u_3 + 1} (α := Set P) (⋂ (y : ι), (↑(s y) : Set P)) (⋂ (i : ι), (↑(s i) : Set P))
⊢ (↑(iInf s) : Set P) = ⋂ (i : ι), (↑(s i) : Set P)

Tactic:
rw [iInf, coe_sInf, Set.biInter_range]

Premises used: iInf, Set.biInter_range, AffineSubspace.coe_sInf
-- 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 : ι → AffineSubspace k P
p : P
rw : p ∈ sInf (range s) ↔ ∀ (i : ι), p ∈ s i
rw₁ : (∀ s_1 ∈ range s, p ∈ s_1) ↔ ∀ (i : ι), p ∈ s i
rw₂ rw₃ : (∀ (i : ι), p ∈ s i) ↔ ∀ (i : ι), p ∈ s i
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i

Tactic:
rw [iInf, mem_sInf_iff, Set.forall_mem_range]

Premises used: AffineSubspace.mem_sInf_iff, iInf, Set.forall_mem_range
-- 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 : ι → AffineSubspace k P
apply : Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
⊢ (iInf s).direction ≤ ⨅ (i : ι), (s i).direction

Tactic:
apply (direction_sInf _).trans_eq

Premises used: LE.le.trans_eq, AffineSubspace.direction_sInf
-- 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 : ι → AffineSubspace k P
rw rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ (i : ι), (s i).direction) (⨅ (i : ι), (s i).direction)
⊢ Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)

Tactic:
rw [iInf_range]

Premises used: iInf_range
-- 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 : ι → AffineSubspace k P
p : P
h : ∀ (i : ι), p ∈ s i
rw : ∀ s_1 ∈ range s, p ∈ s_1
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction

Tactic:
rw [iInf, direction_sInf_of_mem _ p ?_, iInf_range]

Premises used: iInf, iInf_range, AffineSubspace.direction_sInf_of_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 : ι → AffineSubspace k P
p : P
h rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι), p ∈ s i
⊢ ∀ s_1 ∈ range s, p ∈ s_1

Tactic:
rwa [Set.forall_mem_range]

Premises used: Set.forall_mem_range
-- 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 : ι → AffineSubspace k P
p : P
h : p ∈ iInf s
rw : (sInf (range s)).direction = ⨅ (i : ι), (s i).direction
rw₁ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ s_1 ∈ range s, s_1.direction) (⨅ (i : ι), (s i).direction)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule k V) (⨅ (i : ι), (s i).direction) (⨅ (i : ι), (s i).direction)
⊢ (iInf s).direction = ⨅ (i : ι), (s i).direction

Tactic:
rw [iInf, direction_sInf_of_mem_sInf _ p h, iInf_range]

Premises used: iInf, iInf_range, AffineSubspace.direction_sInf_of_mem_sInf
-- 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₂
⊢ LE.le (α := Submodule k V) (Submodule.span k ((↑s₁ : Set P) -ᵥ (↑s₁ : Set P)))
    (Submodule.span k ((↑s₂ : Set P) -ᵥ (↑s₂ : Set P)))

Tactic:
vectorSpan_mono k h

Premises used: Set.Mem, vectorSpan_mono
-- 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₂
⊢ LE.le (α := Submodule k V) (Submodule.span k ((↑s₁ : Set P) -ᵥ (↑s₁ : Set P)))
    (Submodule.span k ((↑s₂ : Set P) -ᵥ (↑s₂ : Set P)))

Tactic:
exact vectorSpan_mono k h

Premises used: vectorSpan_mono
-- 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:
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: le_sup_left, Set.Subset.trans, sInf_le_sInf, le_sup_right, Set.vsub_self_mono, sup_le