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
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)
h₂ : Eq.{u_5 + 1} (α := k) (Function.const ι 1 i) 1
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) q : k) (1 q : k)
have h₃ : Eq.{u_5 + 1} (α := k) 1 1
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 : Nontrivial ι
i : ι
x : k
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x
have obtain : ∀ (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
Tactic: obtain ⟨j, hij⟩ := exists_ne i
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x
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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x
have hw : s.sum w = 1
Tactic: have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
-- 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 : Nontrivial ι
i : ι
x : k
j : ι
hij : j ≠ i
s : Finset ι := {i, j}
hi : i ∈ s
w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x
hw : s.sum w = 1
⊢ ∃ (a : P), (b.coord i : (a : P) → k) a = x
have h : (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = x
Tactic: use s.affineCombination k b w
-- 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 : Nontrivial ι
i : ι
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)
have intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
Tactic: classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]
-- 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 : Nontrivial ι
i : ι
intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)
have intro₁ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
Tactic: classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]
-- 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 : Nontrivial ι
i : ι
intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₁ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₂ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)
have intro₃ : ∀ (x : k) (j : ι) (hij : j ≠ i),
  let s : Finset ι := {i, j};
  ∀ (hi : i ∈ s), ∃ (a : P), (b.coord i : (a : P) → k) a = x
Tactic: classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]
-- 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 : Nontrivial ι
i : ι
intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₁ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₂ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₃ intro₄ :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s), ∃ (a : P), (b.coord i : (a : P) → k) a = x
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)
have intro₅ : ∀ (x : k) (j : ι) (hij : j ≠ i),
  let s : Finset ι := {i, j};
  ∀ (hi : i ∈ s),
    let w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x;
    ∀ (hw : s.sum w = 1), ∃ (a : P), (b.coord i : (a : P) → k) a = x
Tactic: classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]
-- 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 : Nontrivial ι
i : ι
intro : ∀ (x : k), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₁ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₂ : ∀ (x : k) (j : ι) (hij : j ≠ i), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₃ intro₄ :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s), ∃ (a : P), (b.coord i : (a : P) → k) a = x
intro₅ :
  ∀ (x : k) (j : ι) (hij : j ≠ i),
    let s : Finset ι := {i, j};
    ∀ (hi : i ∈ s),
      let w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x;
      ∀ (hw : s.sum w = 1), ∃ (a : P), (b.coord i : (a : P) → k) a = x
⊢ Function.Surjective.{u_7 + 1, u_5 + 1} (α := P) (β := k) (⇑(b.coord i) : (a : P) → k)
have h : ∀ (x : k) (j : ι) (hij : j ≠ i),
  let s : Finset ι := {i, j};
  ∀ (hi : i ∈ s),
    let w : ι → k := fun (j' : ι) ↦ if j' = i then x else 1 - x;
    ∀ (hw : s.sum w = 1),
      (b.coord i : (a : P) → k) ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) w : P) = x
Tactic: classical
    intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]
-- 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 : ι ≃ ι'
v w : V
⊢ (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) (v + w)) =
    HAdd.hAdd (α := ι → k) (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v) fun (i : ι) ↦
      -((b.basisOf i).sumCoords : (a : V) → k) w
have h : ∀ (x : ι),
  -((b.basisOf x).sumCoords : (a : V) → k) (v + w) =
    HAdd.hAdd (α := ι → k) (β := ι → k) (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v)
      (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) w) x
Tactic: ext
-- 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 : ι ≃ ι'
t : k
v : V
⊢ (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) (t • v)) =
    HSMul.hSMul (α := k) (β := ι → k) ((RingHom.id k : (a : k) → k) t : k) fun (i : ι) ↦
      -((b.basisOf i).sumCoords : (a : V) → k) v
have h : ∀ (x : ι),
  -((b.basisOf x).sumCoords : (a : V) → k) (t • v) =
    HSMul.hSMul (α := k) (β := ι → k) ((RingHom.id k : (a : k) → k) t : k)
      (fun (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v) x
Tactic: ext
-- 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 : ι ≃ ι'
p : P
v : V
⊢ (fun (i : ι) ↦ (b.coord i : (a : P) → k) (v +ᵥ p)) =
    HVAdd.hVAdd (α := ι → k) (β := ι → k)
      (({ toFun := fun (v : V) (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v, map_add' := ⋯, map_smul' := ⋯ :
              V →ₗ[k] ι → k } :
            (a : V) → ι → k)
          v :
        ι → k)
      fun (i : ι) ↦ (b.coord i : (a : P) → k) p
have h : ∀ (x : ι),
  (b.coord x : (a : P) → k) (v +ᵥ p) =
    HVAdd.hVAdd (α := ι → k) (β := ι → k)
      (({ toFun := fun (v : V) (i : ι) ↦ -((b.basisOf i).sumCoords : (a : V) → k) v, map_add' := sorry, map_smul' := sorry :
              V →ₗ[k] ι → k } :
            (a : V) → ι → k)
          v :
        ι → k)
      (fun (i : ι) ↦ (b.coord i : (a : P) → k) p) x
Tactic: ext
-- 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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤
have rw : Eq.{u_7 + 1} (α := AffineSubspace k P)
  (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
Tactic: rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
rw :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤
have rw₁ : Eq (α := AffineSubspace k P)
  (affineSpan k (HVAdd.hVAdd (β := Set P) x (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))) ⊤
Tactic: rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
rw :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
rw₁ :
  Eq (α := AffineSubspace k P)
    (affineSpan k (HVAdd.hVAdd (β := Set P) x (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))) ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤
have rw₂ : HVAdd.hVAdd (β := AffineSubspace k P) x (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) = ⊤
Tactic: rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
rw :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
rw₁ :
  Eq (α := AffineSubspace k P)
    (affineSpan k (HVAdd.hVAdd (β := Set P) x (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))) ⊤
rw₂ : HVAdd.hVAdd (β := AffineSubspace k P) x (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) = ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤
have rw₃ : HVAdd.hVAdd (β := AffineSubspace k P) x ⊤ = ⊤
Tactic: rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_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_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
x : V
b : AffineBasis ι k P
rw :
  Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range fun (i : ι) ↦ HVAdd.hVAdd (β := P) x ((b : (a : ι) → P) i : P))) ⊤
rw₁ :
  Eq (α := AffineSubspace k P)
    (affineSpan k (HVAdd.hVAdd (β := Set P) x (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))) ⊤
rw₂ : HVAdd.hVAdd (β := AffineSubspace k P) x (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))) = ⊤
rw₃ : HVAdd.hVAdd (β := AffineSubspace k P) x ⊤ = ⊤
⊢ Eq (α := AffineSubspace k P) (affineSpan k (range (HVAdd.hVAdd (β := (a : ι) → P) x (⇑b : (a : ι) → P)))) ⊤
have rw₄ : Eq.{u_7 + 1} (α := AffineSubspace k P) ⊤ ⊤
Tactic: rw [Pi.vadd_def, ← vadd_set_range, ← AffineSubspace.pointwise_vadd_span, b.tot,
        AffineSubspace.pointwise_vadd_top]
-- 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
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).basisOf = b.basisOf
have h : ∀ (x : ι) (i : { j : ι // j ≠ x }),
  Eq.{u_6 + 1} (α := V) (((v +ᵥ b).basisOf x : (a : { j : ι // j ≠ x }) → V) i : V)
    ((b.basisOf x : (a : { j : ι // j ≠ x }) → V) i : V)
Tactic: ext
-- 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
i : ι
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).coord i = (b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P)
have h : ∀ (p : P),
  Eq.{u_5 + 1} (α := k) (((v +ᵥ b).coord i : (a : P) → k) p : k)
    (((b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P) : (a : P) → k) p : k)
Tactic: ext p
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ Eq.{u_5 + 1} (α := k) (((v +ᵥ b).coord i : (a : P) → k) p : k)
    (((b.coord i).comp (↑(AffineEquiv.symm (AffineEquiv.constVAdd k P v)) : P →ᵃ[k] P) : (a : P) → k) p : k)
have h : Eq.{u_5 + 1} (α := k)
  (Finsupp.sum (M := k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)))
    fun (x : { j : ι // ¬j = i }) ↦ id)
  (Finsupp.sum (M := k) (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i))
    fun (x : { j : ι // ¬j = i }) ↦ id)
Tactic: simp only [coord, ne_eq, basisOf_vadd, coe_vadd, Pi.vadd_apply, Basis.coe_sumCoords,
    AffineMap.coe_mk, AffineEquiv.constVAdd_symm, AffineMap.coe_comp, AffineEquiv.coe_toAffineMap,
    Function.comp_apply, AffineEquiv.constVAdd_apply, sub_right_inj]
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ Eq.{u_5 + 1} (α := k)
    (Finsupp.sum (M := k)
      (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k)
        (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)))
      fun (x : { j : ι // ¬j = i }) ↦ id)
    (Finsupp.sum (M := k) (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i))
      fun (x : { j : ι // ¬j = i }) ↦ id)
have h : Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
Tactic: congr! 1
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
⊢ Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
have h : Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (-v + (p -ᵥ (b : (a : ι) → P) i)) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
Tactic: rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
h :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (-v + (p -ᵥ (b : (a : ι) → P) i)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
⊢ Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
have h₁ : Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
Tactic: rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]
-- 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
i : ι
v : V
b : AffineBasis ι k P
p : P
h :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (-v + (p -ᵥ (b : (a : ι) → P) i)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
h₁ :
  Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
⊢ Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ HVAdd.hVAdd (β := P) v ((b : (a : ι) → P) i : P)) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
    (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) ((-v +ᵥ p) -ᵥ (b : (a : ι) → P) i) :
      Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
have h₂ : Eq (α := Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
  (((b.basisOf i).repr : (a : V) → { j : ι // ¬j = i } →₀ k) (p -ᵥ (b : (a : ι) → P) i - v) :
    Finsupp.{u_1, u_5} { j : ι // ¬j = i } k)
Tactic: rw [vadd_vsub_assoc, neg_add_eq_sub, vsub_vadd_eq_vsub_sub]