awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑s : Set P))) ≤ finrank.{u_1, u_2} k ↥s.direction + 1
have pos : finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
  finrank.{u_1, u_2} k ↥s.direction + 1
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
have pos : ∀ (hs : (↑s : Set P) = ∅),
  finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
Tactic: rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
pos :
  ∀ (hs : (↑s : Set P) = ∅),
    finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
      finrank.{u_1, u_2} k ↥s.direction + 1
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
have pos₁ : ∀ (p₀ : P) (hp₀ : p₀ ∈ (↑s : Set P)),
  finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
Tactic: rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : (↑s : Set P) = ∅
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
have hs₁ : s = ⊥
Tactic: rw [coe_eq_bot_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
have pos : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) ≤ 1
Tactic: rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan, direction_bot, finrank_bot,
      zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) ≤ 1
have h : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = 0
Tactic: convert! zero_le_one' ℕ
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = 0
have h : finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥
Tactic: rw [← finrank_bot k V]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥
have h : ∀ (x : V), Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
h : ∀ (x : V), Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥
have h₁ : ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅)) →
  Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring →
    inst_2 ≍ inst_2 → Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
hs : s = ⊥
h : ∀ (x : V), Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
h₁ :
  ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅)) →
    Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring →
      inst_2 ≍ inst_2 → Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (P := P) (insert p ∅)) = finrank.{u_1, u_2} k ↥⊥
have h₂ : ↥⊥ = ↥(vectorSpan k (P := P) (insert p ∅)) →
  HEq (α := AddCommMonoid ↥⊥) (Submodule.addCommMonoid ⊥) (β := AddCommMonoid ↥(vectorSpan k (P := P) (insert p ∅)))
      (Submodule.addCommMonoid (vectorSpan k (P := P) (insert p ∅))) →
    Eq.{u_1 + 1} (α := Semiring k) DivisionSemiring.toSemiring Ring.toSemiring →
      inst_2 ≍ inst_2 → Eq (α := Submodule k V) ⊥ (vectorSpan k (P := P) (insert p ∅))
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(direction (affineSpan k (insert p (↑(affineSpan k (↑s : Set P)) : Set P)))) ≤
    finrank.{u_1, u_2} k ↥s.direction + 1
have pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
Tactic: rw [affineSpan_coe, direction_affineSpan_insert hp₀, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀) ⊔ s.direction) ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
have pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) + finrank.{u_1, u_2} k ↥s.direction ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
Tactic: refine (Submodule.finrank_add_le_finrank_add_finrank _ _).trans ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) + finrank.{u_1, u_2} k ↥s.direction ≤ 1 + finrank.{u_1, u_2} k ↥s.direction
have pos : finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
⊢ finrank.{u_1, u_2} k ↥(k ∙ (p -ᵥ p₀)) ≤ 1
have pos : ∀ (v : ↥(k ∙ (p -ᵥ p₀))),
  ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) sorry) =
      v
Tactic: refine finrank_le_one ⟨p -ᵥ p₀, Submodule.mem_span_singleton_self _⟩ fun v => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v
have h : Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) (↑v : V)
Tactic: have h := v.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
h : Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) (↑v : V)
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v
have h₁ : ∃ (a : k), a • (p -ᵥ p₀) = (↑v : V)
Tactic: rw [Submodule.mem_span_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
h : ∃ (a : k), a • (p -ᵥ p₀) = (↑v : V)
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v
have pos : ∀ (c : k) (hc : c • (p -ᵥ p₀) = (↑v : V)),
  ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) sorry) =
      v
Tactic: rcases h with ⟨c, hc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
⊢ ∃ (c : k),
    HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
      v
have pos : HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
    (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) sorry) =
  v
Tactic: refine ⟨c, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : AffineSubspace k P
p : P
hf : FiniteDimensional.{u_1, u_2} k ↥s.direction
p₀ : P
hp₀ : p₀ ∈ (↑s : Set P)
v : ↥(k ∙ (p -ᵥ p₀))
c : k
hc : c • (p -ᵥ p₀) = (↑v : V)
⊢ HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
      (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) ⋯) =
    v
have pos : (↑(HSMul.hSMul (β := ↥(k ∙ (p -ᵥ p₀))) c
        (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Submodule k V) (k ∙ (p -ᵥ p₀)) x) (p -ᵥ p₀) sorry)) :
    V) =
  (↑v : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
p : P
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ finrank.{u_1, u_2} k ↥(vectorSpan k s) + 1
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k (insert p (↑(affineSpan k s) : Set P))) ≤
  finrank.{u_1, u_2} k ↥(direction (affineSpan k s)) + 1
Tactic: rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan,
    ← direction_affineSpan _ s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p : P
⊢ Coplanar k (insert p s)
have this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
Tactic: have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
⊢ Coplanar k (insert p s)
have grw : finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ 2
Tactic: grw [coplanar_iff_finrank_le_two, finrank_vectorSpan_insert_le_set, h.finrank_le_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
grw : finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ 2
⊢ Coplanar k (insert p s)
have grw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k s) + 1 ≤ 2
Tactic: grw [coplanar_iff_finrank_le_two, finrank_vectorSpan_insert_le_set, h.finrank_le_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k s)
grw : finrank.{u_1, u_2} k ↥(vectorSpan k (insert p s)) ≤ 2
grw₁ : finrank.{u_1, u_2} k ↥(vectorSpan k s) + 1 ≤ 2
⊢ Coplanar k (insert p s)
have grw₂ : HAdd.hAdd (α := ℕ) 1 1 ≤ HAdd.hAdd (α := ℕ) 1 1
Tactic: grw [coplanar_iff_finrank_le_two, finrank_vectorSpan_insert_le_set, h.finrank_le_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : finrank k V = 2
⊢ Coplanar k s
have this : FiniteDimensional k V
Tactic: have : FiniteDimensional k V := .of_finrank_eq_succ h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s : Set P
h : finrank k V = 2
this : FiniteDimensional k V
⊢ Coplanar k s
have rw : finrank.{u_1, u_2} k ↥(vectorSpan k s) ≤ finrank k V
Tactic: rw [coplanar_iff_finrank_le_two, ← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ Collinear k (P := P) {s.points i, s.centroid, s.faceOppositeCentroid i}
have h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i}) (s.points i)
Tactic: apply collinear_insert_of_mem_affineSpan_pair
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i}) (s.points i)
have h : s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
Tactic: have h : s.points i = (-n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid := by
    rw [← neg_vsub_eq_vsub_rev, neg_smul_neg, ← point_vsub_centroid_eq_smul_vsub, vsub_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
h : s.points i = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i}) (s.points i)
have h₁ : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.centroid, s.faceOppositeCentroid i})
  (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-(↑n : k)) (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
⊢ Nonempty (AffineBasis ι k P)
have obtain : ∀ (s : Set P) (b : AffineBasis (↑s : Type u₄) k P)
  (hb : Eq (α := (a : (↑s : Type u₄)) → P) (⇑b : (a : (↑s : Type u₄)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))),
  Nonempty (AffineBasis ι k P)
Tactic: obtain ⟨s, b, hb⟩ := AffineBasis.exists_affineBasis k V P
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Set P
b : AffineBasis (↑s : Type u₄) k P
hb : Eq (α := (a : (↑s : Type u₄)) → P) (⇑b : (a : (↑s : Type u₄)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ Nonempty (AffineBasis ι k P)
have lift : ∀ (s : Finset P) (b : AffineBasis (↑(↑s : Set P) : Type u₄) k P)
  (hb :
    Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
      (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))),
  Nonempty (AffineBasis ι k P)
Tactic: lift s to Finset P using b.finite_set
Cleared hypotheses: s, b, hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
⊢ Nonempty (AffineBasis ι k P)
have refine : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card ι
Tactic: refine ⟨b.reindex <| Fintype.equivOfCardEq ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
⊢ Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card ι
have rw : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Module.finrank k V + 1
Tactic: rw [h, ← b.card_eq_finrank_add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
inst_4 : Fintype ι
inst_5 : FiniteDimensional k V
h : Fintype.card ι = Module.finrank k V + 1
s : Finset P
b : AffineBasis (↑(↑s : Set P) : Type u₄) k P
hb :
  Eq (α := (a : (↑(↑s : Set P) : Type u₄)) → P) (⇑b : (a : (↑(↑s : Set P) : Type u₄)) → P)
    (Subtype.val (p := fun (x : P) ↦ x ∈ (↑s : Set P)))
rw : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Module.finrank k V + 1
⊢ Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card ι
have rw₁ : Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄) = Fintype.card.{u₄} (↑(↑s : Set P) : Type u₄)
Tactic: rw [h, ← b.card_eq_finrank_add_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Module.Finite R V
inst_5 : Module.Free R V
inst_6 : AffineSpace V P
inst_7 : AddCommGroup W
inst_8 : Module R W
inst_9 : Module S W
inst_10 : Module.Finite S W
inst_11 : SMulCommClass R S W
inst_12 : Module.Free S W
inst_13 : StrongRankCondition R
inst_14 : StrongRankCondition S
⊢ Module.finrank S (W × (V →ₗ[R] W)) = (Module.finrank R V + 1) * Module.finrank S W
have rw : Module.finrank S W + Module.finrank R V * Module.finrank S W = (Module.finrank R V + 1) * Module.finrank S W
Tactic: rw [Module.finrank_prod, Module.finrank_linearMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (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
ι : Type u_4
inst_4 : Fintype ι
p : ι → P
⊢ AffineIndependent k p ↔
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
have mp : AffineIndependent k p →
  ∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (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
ι : Type u_4
inst_4 : Fintype ι
p : ι → P
mp :
  AffineIndependent k p →
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
⊢ AffineIndependent k p ↔
    ∀ (w : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
        Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0
have mpr : (∀ (w : ι → k),
    Eq.{u_1 + 1} (α := k) (∑ i : ι, w i) 0 →
      Eq.{u_2 + 1} (α := V) ((weightedVSub univ p : (a : ι → k) → V) w : V) (0 : V) → ∀ (i : ι), w i = 0) →
  AffineIndependent k p
Tactic: constructor