awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
i j : ι
h : i ≠ j
rw :
  Eq.{u_5 + 1} (α := k)
    (({
            toFun := fun (q : P) ↦
              HSub.hSub (α := k) (β := k) (1 : k)
                (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k),
            linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ } :
          (a : P) → k)
        ((b : (a : ι) → P) j : P) :
      k)
    (0 : k)
rw₁ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) j : P) ((b : (a : ι) → P) i : P)) :
        k) =
    0
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (0 : k)
have rw₂ : HSub.hSub (α := k) (β := k) (1 : k)
    (((b.basisOf i).sumCoords : (a : V) → k)
        (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j sorry) : ι) : P)
          ((b : (a : ι) → P) i : P)) :
      k) =
  0
Tactic: rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
i j : ι
h : i ≠ j
rw :
  Eq.{u_5 + 1} (α := k)
    (({
            toFun := fun (q : P) ↦
              HSub.hSub (α := k) (β := k) (1 : k)
                (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k),
            linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ } :
          (a : P) → k)
        ((b : (a : ι) → P) j : P) :
      k)
    (0 : k)
rw₁ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) j : P) ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₂ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : ι) : P)
            ((b : (a : ι) → P) i : P)) :
        k) =
    0
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (0 : k)
have rw₃ : HSub.hSub (α := k) (β := k) (1 : k)
    (((b.basisOf i).sumCoords : (a : V) → k)
        ((b.basisOf i : (a : { j : ι // j ≠ i }) → V) (Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j sorry) : V) :
      k) =
  0
Tactic: rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
i j : ι
h : i ≠ j
rw :
  Eq.{u_5 + 1} (α := k)
    (({
            toFun := fun (q : P) ↦
              HSub.hSub (α := k) (β := k) (1 : k)
                (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k),
            linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ } :
          (a : P) → k)
        ((b : (a : ι) → P) j : P) :
      k)
    (0 : k)
rw₁ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) j : P) ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₂ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : ι) : P)
            ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₃ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          ((b.basisOf i : (a : { j : ι // j ≠ i }) → V) (Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : V) :
        k) =
    0
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (0 : k)
have rw₄ : HSub.hSub (α := k) 1 1 = 0
Tactic: rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
i j : ι
h : i ≠ j
rw :
  Eq.{u_5 + 1} (α := k)
    (({
            toFun := fun (q : P) ↦
              HSub.hSub (α := k) (β := k) (1 : k)
                (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k),
            linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ } :
          (a : P) → k)
        ((b : (a : ι) → P) j : P) :
      k)
    (0 : k)
rw₁ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) j : P) ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₂ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          (VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑(Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : ι) : P)
            ((b : (a : ι) → P) i : P)) :
        k) =
    0
rw₃ :
  HSub.hSub (α := k) (β := k) (1 : k)
      (((b.basisOf i).sumCoords : (a : V) → k)
          ((b.basisOf i : (a : { j : ι // j ≠ i }) → V) (Subtype.mk (p := fun (x : ι) ↦ x ≠ i) j ⋯) : V) :
        k) =
    0
rw₄ : HSub.hSub (α := k) 1 1 = 0
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (0 : k)
have rw₅ : Eq.{u_5 + 1} (α := k) 0 0
Tactic: rw [coord, AffineMap.coe_mk, ← Subtype.coe_mk (p := (· ≠ i)) j h.symm, ← b.basisOf_apply,
    Basis.sumCoords_self_apply, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : DecidableEq ι
i j : ι
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
have inl : ∀ (h : i = j),
  Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
Tactic: rcases eq_or_ne i j with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : DecidableEq ι
i j : ι
inl :
  ∀ (h : i = j),
    Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
have inr : ∀ (h : i ≠ j),
  Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) ((b : (a : ι) → P) j : P) : k) (if i = j then 1 else 0 : k)
Tactic: rcases eq_or_ne i j with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
q : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
have rw : Membership.mem (γ := AffineSubspace k P) ⊤ q
Tactic: rw [b.tot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
q : P
⊢ Eq.{u_5 + 1} (α := k) (∑ i : ι, (b.coord i : (a : P) → k) q) 1
have hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
Tactic: have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
⊢ Eq.{u_5 + 1} (α := k) (∑ i : ι, (b.coord i : (a : P) → k) q) 1
have obtain : ∀ (w : ι → k) (hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1)
  (hq :
    Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
      ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)),
  Eq.{u_5 + 1} (α := k)
    (∑ i : ι,
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P))
    1
Tactic: obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
⊢ Eq.{u_5 + 1} (α := k)
    (∑ i : ι,
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P))
    1
have h : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x →
    (b.coord x : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) =
      w x
Tactic: convert! hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
q : P
⊢ ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
      (b.coord i : (a : P) → k) q) =
    q
have hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
Tactic: have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
q : P
hq : Membership.mem (γ := AffineSubspace k P) (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) q
⊢ ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
      (b.coord i : (a : P) → k) q) =
    q
have obtain : ∀ (w : ι → k) (hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1)
  (hq :
    Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
      (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
      ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)),
  Eq.{u_7 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k)
          ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) :
      P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
Tactic: obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
⊢ Eq.{u_7 + 1} (α := P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b.coord i : (a : P) → k)
          ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) :
      P)
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
have h : (fun (i : ι) ↦
    (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)) =
  w
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Fintype ι
w : ι → k
hw : Eq.{u_5 + 1} (α := k) (∑ i : ι, w i) 1
hq :
  Membership.mem.{u_7, u_7} (α := P) (γ := AffineSubspace k P)
    (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
    ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)
⊢ (fun (i : ι) ↦
      (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P)) =
    w
have h : ∀ (i : ι),
  (b.coord i : (a : P) → k) ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = w i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Fintype ι
b : AffineBasis ι k V
v : V
⊢ ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) = v
have hb : ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → V) : (a : ι → k) → V) fun (i : ι) ↦
    (b.coord i : (a : V) → k) v) =
  v
Tactic: have hb := b.affineCombination_coord_eq_self v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Fintype ι
b : AffineBasis ι k V
v : V
hb :
  ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → V) : (a : ι → k) → V) fun (i : ι) ↦
      (b.coord i : (a : V) → k) v) =
    v
⊢ ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) = v
have rwa : ∀
  (hb :
    ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) =
      v),
  ∑ i : ι, HSMul.hSMul.{u_5, u_6, u_6} (α := k) (β := V) ((b.coord i : (a : V) → k) v : k) ((b : (a : ι) → V) i : V) = v
Tactic: rwa [Finset.univ.affineCombination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v)] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q₁ : k) ((b.coord i : (a : P) → k) q₂ : k)
⊢ q₁ = q₂
have intro : ∀ (val : Fintype ι), q₁ = q₂
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q₁ : k) ((b.coord i : (a : P) → k) q₂ : k)
val : Fintype ι
⊢ q₁ = q₂
have intro : Eq.{u_7 + 1} (α := P)
  ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
      (b.coord i : (a : P) → k) q₁ :
    P)
  ((Finset.affineCombination k Finset.univ (⇑b : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
      (b.coord i : (a : P) → k) q₂ :
    P)
Tactic: rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
⊢ Eq (α := (a : P) → k) (⇑(b.coord i) : (a : P) → k) 1
have h : ∀ (q : P), Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
Tactic: ext q
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
have rw : Set.Subsingleton.{u_7} (α := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
⊢ Set.Subsingleton.{u_7} (α := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ)
have hs : Set.Subsingleton.{u_1} (α := ι) univ
Tactic: apply Subsingleton.image
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
Tactic: have hp : (range b).Subsingleton := by
    rw [← image_univ]
    apply Subsingleton.image
    apply subsingleton_of_subsingleton
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have this : Subsingleton P
Tactic: haveI := AffineSubspace.subsingleton_of_subsingleton_span_eq_top hp b.tot
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have hi : i ∈ s
Tactic: have hi : i ∈ s := by simp [s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
Tactic: have hw : s.sum (Function.const ι (1 : k)) = 1 := by simp [s]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (hypothesis)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have hq : q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)
Tactic: have hq : q = s.affineCombination k b (Function.const ι (1 : k)) := by
    simp [eq_iff_true_of_subsingleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
hq : q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have h : Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 : k)
Tactic: rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
hq : q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)
h : Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 : k)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have h₁ : Eq.{u_5 + 1} (α := k)
  ((b.coord i : (a : P) → k)
      ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1) : P) :
    k)
  (1 : k)
Tactic: rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : Subsingleton ι
i : ι
q : P
hp : Set.Subsingleton.{u_7} (α := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
this : Subsingleton P
s : Finset ι := {i}
hi : i ∈ s
hw : Eq.{u_5 + 1} (α := k) (s.sum (Function.const ι 1)) 1
hq : q = (Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1)
h : Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 : k)
h₁ :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Function.const ι 1) : P) :
      k)
    (1 : k)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have h₂ : Eq.{u_5 + 1} (α := k) (Function.const ι 1 i) 1
Tactic: rw [Pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw, Function.const_apply]