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
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 ≠ ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw₄ : s.Nonempty ↔ s ≠ ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    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
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 ≠ ∅
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s = ∅
have rw₅ : s ≠ ∅ ↔ s ≠ ∅
Tactic: rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
    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
inst_3 : AffineSpace V P
s : Set P
⊢ LT.lt (α := AffineSubspace k P) ⊥ (affineSpan k s) ↔ s.Nonempty
have rw : Ne (α := AffineSubspace k P) (affineSpan k s) ⊥ ↔ s ≠ ∅
Tactic: rw [bot_lt_iff_ne_bot, 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
inst_3 : AffineSpace V P
s : Set P
inst_4 : Subsingleton P
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ s.Nonempty
have rw : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ LT.lt (α := AffineSubspace k P) ⊥ (affineSpan k s)
Tactic: rw [← bot_lt_affineSpan k, IsSimpleOrder.bot_lt_iff_eq_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
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)
⊢ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ s.Nonempty
have rw₁ : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤ ↔ Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
Tactic: rw [← bot_lt_affineSpan k, IsSimpleOrder.bot_lt_iff_eq_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
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
⊢ p x h
have suffices : ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
Tactic: suffices ∃ (hx : x ∈ affineSpan k s), p x hx from this.elim fun hx hc ↦ hc
-- 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
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
⊢ ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
have mem₁ : ∀ x ∈ s, ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
Tactic: refine affineSpan_induction h ?mem ?smul_vsub_vadd
-- 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
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
mem₁ : ∀ x ∈ s, ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
⊢ ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) x), p x hx
have smul_vsub_vadd₁ : ∀ (c : k) (u v w : P),
  (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) u), p u hx) →
    (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) v), p v hx) →
      (∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) w), p w hx) →
        ∃ (hx : Membership.mem (γ := AffineSubspace k P) (affineSpan k s) (c • (u -ᵥ v) +ᵥ w)), p (c • (u -ᵥ v) +ᵥ w) hx
Tactic: refine affineSpan_induction h ?mem ?smul_vsub_vadd
-- 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
inst_3 : AffineSpace V P
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ affineSpan k {p₁, p₂} ≤ s
have rw : p₁ ∈ (↑s : Set P) ∧ p₂ ∈ (↑s : Set P)
Tactic: rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_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
inst_3 : AffineSpace V P
p : P
ps : Set P
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
have rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
Tactic: rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
have rw₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k ({p} ∪ ps))
Tactic: rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k ({p} ∪ ps))
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
have rw₂ : Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ({p} ∪ ps))
Tactic: rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k ({p} ∪ ps))
rw₂ :
  Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ({p} ∪ ps))
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
have rw₃ : Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P))
  (affineSpan k {p} ⊔ affineSpan k ps)
Tactic: rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
rw : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k ({p} ∪ (↑(affineSpan k ps) : Set P))) (affineSpan k ({p} ∪ ps))
rw₂ :
  Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ({p} ∪ ps))
rw₃ :
  Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k (↑(affineSpan k ps) : Set P))
    (affineSpan k {p} ⊔ affineSpan k ps)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k (insert p ps))
have rw₄ : Eq (α := AffineSubspace k P) (affineSpan k {p} ⊔ affineSpan k ps) (affineSpan k {p} ⊔ affineSpan k ps)
Tactic: rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k ps) p
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p ps)) (affineSpan k ps)
have h₁ : p ∈ (↑(affineSpan k ps) : Set P)
Tactic: rw [← mem_coe] 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
inst_3 : AffineSpace V P
p : P
ps : Set P
h : p ∈ (↑(affineSpan k ps) : Set P)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p ps)) (affineSpan k ps)
have rw : Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k ps)
Tactic: rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
h : p ∈ (↑(affineSpan k ps) : Set P)
rw : Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k ps)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p ps)) (affineSpan k ps)
have rw₁ : Eq (α := AffineSubspace k P) (affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ps)
Tactic: rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
h : p ∈ (↑(affineSpan k ps) : Set P)
rw : Eq (α := AffineSubspace k P) (affineSpan k (insert p (↑(affineSpan k ps) : Set P))) (affineSpan k ps)
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k (↑(affineSpan k ps) : Set P)) (affineSpan k ps)
⊢ Eq (α := AffineSubspace k P) (affineSpan k (insert p ps)) (affineSpan k ps)
have rw₂ : Eq (α := AffineSubspace k P) (affineSpan k ps) (affineSpan k ps)
Tactic: rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]
-- 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
inst_3 : AffineSpace V P
p : P
ps : Set P
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k ps) p
⊢ Eq (α := Submodule k V) (vectorSpan k (insert p ps)) (vectorSpan k ps)
have simp_rw : Eq (α := Submodule k V) (direction (affineSpan k (insert p ps))) (direction (affineSpan k ps))
Tactic: simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
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
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u -ᵥ v) +ᵥ w)
have smul_vsub_vadd : Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v) + w)
Tactic: simp only [vsub_eq_sub, vadd_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
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
c : k
u : V
hu_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u
v : V
hv_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v
w : V
hw_1 : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w
hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u
hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v
hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v) + w)
have apply : Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u - v))
Tactic: apply Submodule.add_mem _ _ hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
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
hx : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) x
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) x
have mem : ∀ (x : V) (hx : x ∈ s), Membership.mem (γ := Submodule k V) (Submodule.span k s) x
Tactic: induction hx using affineSpan_induction' with
  | mem x hx => exact Submodule.subset_span hx
  | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
    simp only [vsub_eq_sub, vadd_eq_add]
    apply Submodule.add_mem _ _ hw
    exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
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
hx : Membership.mem (γ := AffineSubspace k V) (affineSpan k s) x
mem : ∀ (x : V) (hx : x ∈ s), Membership.mem (γ := Submodule k V) (Submodule.span k s) x
⊢ Membership.mem (γ := Submodule k V) (Submodule.span k s) x
have smul_vsub_vadd : ∀ (c : k) (u : V),
  Membership.mem (γ := AffineSubspace k V) (affineSpan k s) u →
    ∀ (v : V),
      Membership.mem (γ := AffineSubspace k V) (affineSpan k s) v →
        ∀ (w : V),
          Membership.mem (γ := AffineSubspace k V) (affineSpan k s) w →
            ∀ (hu : Membership.mem (γ := Submodule k V) (Submodule.span k s) u)
              (hv : Membership.mem (γ := Submodule k V) (Submodule.span k s) v)
              (hw : Membership.mem (γ := Submodule k V) (Submodule.span k s) w),
              Membership.mem (γ := Submodule k V) (Submodule.span k s) (c • (u -ᵥ v) +ᵥ w)
Tactic: induction hx using affineSpan_induction' with
  | mem x hx => exact Submodule.subset_span hx
  | smul_vsub_vadd c u _ v _ w _ hu hv hw =>
    simp only [vsub_eq_sub, vadd_eq_add]
    apply Submodule.add_mem _ _ hw
    exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k s) : Set V)
have rw : (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k (insert 0 s)) : Set V)
Tactic: rw [← Submodule.span_insert_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(affineSpan k (insert 0 s)) : Set V) = (↑(Submodule.span k (insert 0 s)) : Set V)
have refine : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(affineSpan k (insert 0 s)) : Set V)
Tactic: refine affineSpan_subset_span.antisymm ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(affineSpan k (insert 0 s)) : Set V)
have rw : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V) + insert 0 s
Tactic: rw [← vectorSpan_add_self, vectorSpan_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V) + insert 0 s
have refine : (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V)
Tactic: refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
s : Set V
⊢ (↑(Submodule.span k (insert 0 s)) : Set V) ⊆ (↑(Submodule.span k (insert 0 s -ᵥ insert 0 s)) : Set V)
have _a : insert 0 s ⊆ insert 0 s -ᵥ insert 0 s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
f g : AffineBasis ι k P
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : ι → P) (ind' : AffineIndependent k toFun)
  (tot' : Eq (α := AffineSubspace k P) (affineSpan k (range toFun)) ⊤)
  (h : { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun = g.toFun),
  { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
g : AffineBasis ι k P
toFun : ι → P
ind' : AffineIndependent k toFun
tot' : Eq (α := AffineSubspace k P) (affineSpan k (range toFun)) ⊤
h : { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun = g.toFun
⊢ { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } = g
have mk : ∀ (toFun_1 : ι → P) (ind'_1 : AffineIndependent k toFun_1)
  (tot'_1 : Eq (α := AffineSubspace k P) (affineSpan k (range toFun_1)) ⊤)
  (h :
    { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P }.toFun =
      { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 : AffineBasis ι k P }.toFun),
  { toFun := toFun, ind' := ind', tot' := tot' : AffineBasis ι k P } =
    { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e_1 e : ι ≃ ι'
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k
      (range.{u_7, u_2 + 1} (ι := ι')
        (Function.comp.{u_2 + 1, u_1 + 1, u_7 + 1} (β := ι) (⇑b : (a : ι) → P) (⇑e.symm : (a : ι') → ι))))
    ⊤
have rw : Eq.{u_7 + 1} (α := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) ⊤
Tactic: rw [e.symm.surjective.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
this :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))
have rw : LE.le (α := Submodule k V) ⊤ (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
Tactic: rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
this :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw :
  LE.le (α := Submodule k V) ⊤
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))
have rw₁ : LE.le (α := Submodule k V) ⊤
  (AffineSubspace.direction.{u_5, u_6, u_7} (P := P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))))
Tactic: rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]