awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
have rw : s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
Tactic: rw [lt_iff_le_not_ge, not_le_iff_exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
rw : s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
⊢ s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
have rw₁ : (s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
Tactic: rw [lt_iff_le_not_ge, not_le_iff_exists]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p : P
⊢ Eq (α := AffineSubspace k P) (mk' p ⊤) ⊤
have h : ∀ (x : P), Membership.mem (γ := AffineSubspace k P) (mk' p ⊤) x ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
have obtain : ∀ (p : P), Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
Tactic: obtain ⟨p⟩ := S.nonempty
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
p : P
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
have h : ∀ (v : V),
  Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v ↔ Membership.mem (γ := Submodule k V) ⊤ v
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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
have h : ∀ (_hv : Membership.mem (γ := Submodule k V) ⊤ v),
  Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v
Tactic: refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
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
have hpv : 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 _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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)
⊢ Membership.mem (γ := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) v
have 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
Tactic: rwa [vadd_vsub] at hpv
Cleared hypotheses: hpv
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
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) ⊥ ⊤
⊢ False
have contra₁ : Eq.{u_3 + 1} (α := Set P) ∅ univ
Tactic: rw [AffineSubspace.ext_iff, bot_coe, top_coe] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ s.Nonempty
have rw : s ≠ ∅
Tactic: rw [Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
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 ∅) ⊤
⊢ False
have h₁ : Eq.{u_3 + 1} (α := AffineSubspace k P) ⊥ ⊤
Tactic: rw [AffineSubspace.span_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have rw : Eq (α := Submodule k V) (direction (affineSpan k s)) ⊤
Tactic: rw [← direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
h : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
rw : Eq (α := Submodule k V) (direction (affineSpan k s)) ⊤
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have rw₁ : Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊤) ⊤
Tactic: rw [← direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ⊤) ⊤
⊢ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have rw₂ : Eq.{u_2 + 1} (α := Submodule k V) ⊤ ⊤
Tactic: rw [← direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
hs : s.Nonempty
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have refine : Eq (α := Submodule k V) (vectorSpan k s) ⊤ → Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
Tactic: refine ⟨vectorSpan_eq_top_of_affineSpan_eq_top k V P, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have obtain : ∀ (p : P) (hp : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) p),
  Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
Tactic: obtain ⟨p, hp : p ∈ affineSpan k s⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have rw : Eq (α := Submodule k V) (direction (affineSpan k s)) (direction.{u_1, u_2, u_3} (P := P) ⊤)
Tactic: rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ⊤)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have rw₁ : Eq (α := Submodule k V) (vectorSpan k s) (direction.{u_1, u_2, u_3} (P := P) ⊤)
Tactic: rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ⊤)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have rw₂ : Eq (α := Submodule k V) ⊤ (direction.{u_1, u_2, u_3} (P := P) ⊤)
Tactic: rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ⊤)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have rw₃ : Eq.{u_2 + 1} (α := Submodule k V) ⊤ ⊤
Tactic: rw [eq_iff_direction_eq_of_mem hp (mem_top k V p), direction_affineSpan, h, direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
have suffices : Nonempty.{u_3 + 1} ↥(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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
hs : s.Nonempty
h : Eq (α := Submodule k V) (vectorSpan k s) ⊤
⊢ Nonempty.{u_3 + 1} ↥(affineSpan k s)
have obtain : ∀ (x : P) (hx : x ∈ s), Nonempty.{u_3 + 1} ↥(affineSpan k s)
Tactic: obtain ⟨x, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
inst_3 : Nontrivial P
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have inl : ∀ (hs : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have inr : ∀ (hs : s.Nonempty), Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
Tactic: rcases s.eq_empty_or_nonempty with hs | hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : Set P
inst_3 : Nontrivial P
hs : s.Nonempty
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
have inr : Eq (α := Submodule k V) (vectorSpan k s) ⊤ ↔ Eq (α := Submodule k V) (vectorSpan k s) ⊤
Tactic: rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Type u_5
inst_3 : Fintype ι
p : ι → P
h : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
⊢ 0 < Fintype.card ι
have obtain : ∀ (i : ι), 0 < Fintype.card ι
Tactic: obtain ⟨-, ⟨i, -⟩⟩ := nonempty_of_affineSpan_eq_top k V P h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥
have rw : Eq (α := Submodule k V) (vectorSpan k (↑⊥ : Set P)) ⊥
Tactic: rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
rw : Eq (α := Submodule k V) (vectorSpan k (↑⊥ : Set P)) ⊥
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥
have rw₁ : Eq (α := Submodule k V) (vectorSpan.{u_1, u_2, u_3} k (P := P) ∅) ⊥
Tactic: rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ∅) ⊥
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥
have rw₂ : Eq (α := Submodule k V) (Submodule.span k (VSub.vsub.{u_2, u_3} (P := Set P) ∅ ∅)) ⊥
Tactic: rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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) ∅ ∅)) ⊥
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥
have rw₃ : Eq.{u_2 + 1} (α := Submodule k V) (Submodule.span k ∅) ⊥
Tactic: rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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 ∅) ⊥
⊢ Eq (α := Submodule k V) (direction.{u_1, u_2, u_3} (P := P) ⊥) ⊥
have rw₄ : Eq.{u_2 + 1} (α := Submodule k V) ⊥ ⊥
Tactic: rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ (↑Q : Set P).Nonempty ↔ Q ≠ ⊥
have rw : (↑Q : Set P) ≠ ∅ ↔ Q ≠ ⊥
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ (↑Q : Set P).Nonempty
have rw : Q = ⊥ ∨ Q ≠ ⊥
Tactic: rw [nonempty_iff_ne_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
p₁ p₂ : P
inst_3 : Subsingleton P
s : AffineSubspace k P
⊢ s = ⊥ ∨ s = ⊤
have rw : (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
Tactic: rw [← coe_eq_bot_iff, ← coe_eq_univ_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
ι : Sort u_4
p₁ p₂ : P
inst_3 : Subsingleton P
s : AffineSubspace k P
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
have inl : ∀ (h : (↑s : Set P) = ∅), (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
Tactic: rcases (s : Set P).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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
⊢ (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
have inr : ∀ (h : (↑s : Set P).Nonempty), (↑s : Set P) = ∅ ∨ (↑s : Set P) = univ
Tactic: rcases (s : Set P).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
⊢ s.direction = ⊤ ↔ s = ⊤
have mp : s.direction = ⊤ → s = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s : AffineSubspace k P
h : (↑s : Set P).Nonempty
mp : s.direction = ⊤ → s = ⊤
⊢ s.direction = ⊤ ↔ s = ⊤
have mpr : s = ⊤ → s.direction = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (hypothesis)
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 = ⊤
have hd₁ : s.direction = direction.{u_1, u_2, u_3} (P := P) ⊤
Tactic: rw [← direction_top k V P] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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 = ⊤
have mp : ((↑s : Set P) ∩ (↑⊤ : Set P)).Nonempty
Tactic: refine ext_of_direction_eq hd ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
have h : ∀ (v : V), v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
have h : v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ∧ v ∈ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
have h₃ : v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v ∈ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
have h₄ : v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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₂
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
have h₅ : v +ᵥ p ∈ s₁ ⊓ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
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₂
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
have h₆ : v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂ ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
⊢ (sInf t).direction = ⨅ s ∈ t, s.direction
have apply : ⨅ s ∈ t, s.direction ≤ (sInf t).direction
Tactic: apply (direction_sInf t).antisymm