awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Combination (goal)
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : (↑s : Type u_4) → kˣ
this : s = Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
h :
  ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
        ((t.weightedVSubOfPoint (P := P)
                (fun (q : (↑s : Type u_4)) ↦ ((AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k) : P))
                ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
                    (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
                  P) :
              (a : { x : P // x ∈ s } → k) → V)
            μ :
          V)
        ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
            (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
          P) =
      HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((t.weightedVSubOfPoint (Subtype.val (p := fun (x : P) ↦ x ∈ s))
                (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) :
              (a : { x : P // x ∈ s } → k) → V)
            fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x) : k) :
          V)
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P)
⊢ Eq.{u_4 + 1} (α := AffineSubspace k P)
    (affineSpan k (Set.range fun (q : (↑s : Type u_4)) ↦ (AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k)))
    (affineSpan k (Set.range (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))))
have h₁ : ∀ (t : Finset { x : P // x ∈ s }) (μ : { x : P // x ∈ s } → k),
  HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((t.weightedVSubOfPoint (Subtype.val (p := fun (x : P) ↦ x ∈ s))
              (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) :
            (a : { x : P // x ∈ s } → k) → V)
          μ :
        V)
      (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
    HVAdd.hVAdd.{u_3, u_4, u_4} (α := V) (β := P)
      ((t.weightedVSubOfPoint (P := P)
              (fun (q : (↑s : Type u_4)) ↦ ((AffineMap.lineMap p (↑q : P) : (a : k) → P) (↑(w q) : k) : P))
              ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
                  (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
                P) :
            (a : { x : P // x ∈ s } → k) → V)
          fun (x : { x : P // x ∈ s }) ↦ μ x * (↑(w x)⁻¹ : k) :
        V)
      ((AffineMap.lineMap p (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) : (a : k) → P)
          (↑(w (Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp)) : k) :
        P)
Tactic: apply le_antisymm
    <;> intro q hq
    <;> rw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
    <;> obtain ⟨t, μ, rfl⟩ := hq
    <;> use t
    <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : P
⊢ FiniteDimensional.{u_1, u_2} k ↥(direction (P := P) (affineSpan k {p}))
have rw : FiniteDimensional.{u_1, u_2} k ↥(vectorSpan k (P := P) {p})
Tactic: rw [direction_affineSpan]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
⊢ Finite ι
have a : Nontrivial ι
Tactic: nontriviality ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
h : Nontrivial ι
⊢ Finite ι
have inhabit : ∀ (inhabited_h : Inhabited ι), Finite ι
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
h : Nontrivial ι
inhabited_h : Inhabited ι
⊢ Finite ι
have hi₁ : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i : { x : ι // x ≠ default }) ↦ p (↑i : ι) -ᵥ p default
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k p default] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
have inl : ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
  FiniteDimensional.{u_1, u_2} k ↥(⊥ ⊔ s₂).direction
Tactic: rcases eq_bot_or_nonempty s₁ with rfl | ⟨p₁, hp₁⟩
Cleared hypotheses: s₁, inst_4
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
inl :
  ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
    FiniteDimensional.{u_1, u_2} k ↥(⊥ ⊔ s₂).direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
have inr : ∀ (p₁ : P) (hp₁ : p₁ ∈ (↑s₁ : Set P)), FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
Tactic: rcases eq_bot_or_nonempty s₁ with rfl | ⟨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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
have inr : ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
  FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ ⊥).direction
Tactic: rcases eq_bot_or_nonempty s₂ with rfl | ⟨p₂, hp₂⟩
Cleared hypotheses: s₂, inst_5
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
inr :
  ∀ [FiniteDimensional.{u_1, u_2} k ↥(direction.{u_1, u_2, u_3} (P := P) ⊥)],
    FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ ⊥).direction
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
have inr₁ : ∀ (p₂ : P) (hp₂ : p₂ ∈ (↑s₂ : Set P)), FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
Tactic: rcases eq_bot_or_nonempty s₂ with rfl | ⟨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
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
s₁ s₂ : AffineSubspace k P
inst_4 : FiniteDimensional.{u_1, u_2} k ↥s₁.direction
inst_5 : FiniteDimensional.{u_1, u_2} k ↥s₂.direction
p₁ : P
hp₁ : p₁ ∈ (↑s₁ : Set P)
p₂ : P
hp₂ : p₂ ∈ (↑s₂ : Set P)
⊢ FiniteDimensional.{u_1, u_2} k ↥(s₁ ⊔ s₂).direction
have inr : FiniteDimensional.{u_1, u_2} k ↥(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))
Tactic: rw [AffineSubspace.direction_sup hp₁ hp₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : AffineSubspace k P
inst_7 : FiniteDimensional.{u_1, u_2} k ↥s.direction
f : P →ᵃ[k] P₂
⊢ FiniteDimensional.{u_1, u_5} k ↥(map f s).direction
have rw : FiniteDimensional.{u_1, u_5} k ↥(Submodule.map f.linear s.direction)
Tactic: rw [map_direction]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
Tactic: have hi' := hi.range.mono (Set.image_subset_range p ↑s)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hc' : #(Finset.image p s) = n + 1
Tactic: have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hn : (Finset.image p s).Nonempty
Tactic: have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
hn : (Finset.image p s).Nonempty
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have rcases : ∀ (p₁ : P) (hp₁ : p₁ ∈ Finset.image p s), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: rcases hn with ⟨p₁, hp₁⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hp₁' : p₁ ∈ p '' (↑s : Set ι)
Tactic: have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)
hc' : #(Finset.image p s) = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hi'₁ : LinearIndependent k (M := V)
  fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
Tactic: rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
Cleared hypotheses: hi', hp₁, hp₁'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' :
  LinearIndependent k (M := V)
    fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
⊢ Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
have rw : #(Finset.image p s) - 1 = n
Tactic: rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' :
  LinearIndependent k (M := V)
    fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have hc₁ : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
Tactic: have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc_1 : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' :
  LinearIndependent k (M := V)
    fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
hc : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have rwa : finrank.{u_1, u_2} k
    ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) =
  n
Tactic: rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc_1 : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' :
  LinearIndependent k (M := V)
    fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
hc : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
rwa :
  finrank.{u_1, u_2} k
      ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) =
    n
rwa₁ : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have rwa₂ : LinearIndepOn k id (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)
Tactic: rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc_1 : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' :
  LinearIndependent k (M := V)
    fun (v : (↑(↑(Finset.image (fun (p : P) ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V) : Type u_2)) ↦ (↑v : V)
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' (↑s : Set ι)
hc : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
rwa :
  finrank.{u_1, u_2} k
      ↥(Submodule.span k (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)) =
    n
rwa₁ : Finset.card.{u_2} (α := V) (Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) = n
rwa₂ : LinearIndepOn k id (↑(Finset.image (fun (x : P) ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁)) : Set V)
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have rwa₃ : n = n
Tactic: rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have have : ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have have₃ : ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
have have₁ have₂ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)),
    finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have₃ :
  ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
    (hc' : #(Finset.image p s) = n + 1), finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
⊢ finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
have have₄ : ∀ (hi' : AffineIndependent k (P := P) fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (hc' : #(Finset.image p s) = n + 1) (hn : (Finset.image p s).Nonempty),
  finrank.{u_1, u_2} k ↥(vectorSpan k (↑(Finset.image p s) : Set P)) = n
Tactic: classical
  have hi' := hi.range.mono (Set.image_subset_range p ↑s)
  have hc' : #(s.image p) = n + 1 := by rwa [s.card_image_of_injective hi.injective]
  have hn : (s.image p).Nonempty := by simp [hc', ← Finset.card_pos]
  rcases hn with ⟨p₁, hp₁⟩
  have hp₁' : p₁ ∈ p '' s := by simpa using hp₁
  rw [affineIndependent_set_iff_linearIndependent_vsub k hp₁', ← Finset.coe_singleton,
    ← Finset.coe_image, ← Finset.coe_sdiff, Finset.sdiff_singleton_eq_erase, ← Finset.coe_image]
    at hi'
  have hc : #(((s.image p).erase p₁).image (· -ᵥ p₁)) = n := by
    rw [Finset.card_image_of_injective _ (vsub_left_injective _), Finset.card_erase_of_mem hp₁]
    exact Nat.pred_eq_of_eq_succ hc'
  rwa [vectorSpan_eq_span_vsub_finset_right_ne k hp₁, finrank_span_finset_eq_card, hc]