awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
this :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw :
  LE.le (α := Submodule k V) ⊤
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw₁ :
  LE.le (α := Submodule k V) ⊤
    (AffineSubspace.direction.{u_5, u_6, u_7} (P := P)
      (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))))
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))
have rw₂ : LE.le (α := Submodule k V) ⊤ (AffineSubspace.direction.{u_5, u_6, u_7} (P := P) ⊤)
Tactic: rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
this :
  Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw :
  LE.le (α := Submodule k V) ⊤
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
rw₁ :
  LE.le (α := Submodule k V) ⊤
    (AffineSubspace.direction.{u_5, u_6, u_7} (P := P)
      (affineSpan k (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))))
rw₂ : LE.le (α := Submodule k V) ⊤ (AffineSubspace.direction.{u_5, u_6, u_7} (P := P) ⊤)
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))
have rw₃ : LE.le.{u_6} (α := Submodule k V) ⊤ ⊤
Tactic: rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
⊢ LE.le.{u_6} (α := Submodule k V) ⊤
    (Submodule.span k
      (range fun (i_2 : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑i_2 : ι) : P) ((b : (a : ι) → P) i : P)))
have k₁ : Eq (α := Submodule k V)
  (Submodule.span k
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
  (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
Tactic: suffices
        Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
        rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
| vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P))
have rw : vectorSpan.{u_5, u_6, u_7} k (P := 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
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
⊢ Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (range.{u_7, u_1 + 1} (ι := ι) (⇑b : (a : ι) → P)))
have conv_rhs : Eq (α := Submodule k V)
  (Submodule.span k
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
  (vectorSpan.{u_5, u_6, u_7} k (P := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ))
Tactic: conv_rhs => rw [← image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
⊢ Eq (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (vectorSpan.{u_5, u_6, u_7} k (P := P) (image.{u_1, u_7} (α := ι) (⇑b : (a : ι) → P) univ))
have rw : Eq.{u_6 + 1} (α := Submodule k V)
  (Submodule.span k
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
  (Submodule.span k ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})))
Tactic: rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
⊢ Eq.{u_6 + 1} (α := Submodule k V)
    (Submodule.span k
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P)))
    (Submodule.span k ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})))
have e_s : Eq.{u_6 + 1} (α := Set V)
  (range fun (j : { x : ι // x ≠ i }) ↦
    VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
  ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i}))
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
⊢ Eq.{u_6 + 1} (α := Set V)
    (range fun (j : { x : ι // x ≠ i }) ↦
      VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
    ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i}))
have e_s : ∀ (v : V),
  Membership.mem (γ := Set V)
      (range fun (j : { x : ι // x ≠ i }) ↦
        VSub.vsub.{u_6, u_7} (P := P) ((b : (a : ι) → P) (↑j : ι) : P) ((b : (a : ι) → P) i : P))
      v ↔
    Membership.mem (γ := Set V)
      ((fun (x : P) ↦ x -ᵥ (b : (a : ι) → P) i) '' image (α := ι) (⇑b : (a : ι) → P) (univ \ {i})) v
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).basisOf i =
    Basis.reindex (ι := { j : ι // j ≠ (e.symm : (a : ι') → ι) i }) (b.basisOf ((e.symm : (a : ι') → ι) i))
      (e.subtypeEquiv (p := fun (j : ι) ↦ j ≠ (e.symm : (a : ι') → ι) i) (q := fun (b : ι') ↦ b ≠ i) ⋯)
have a : ∀ (j : { j : ι' // j ≠ i }),
  Eq.{u_6 + 1} (α := V) (((b.reindex e).basisOf i : (a : { j : ι' // j ≠ i }) → V) j : V)
    ((Basis.reindex (ι := { j : ι // j ≠ (e.symm : (a : ι') → ι) i }) (b.basisOf ((e.symm : (a : ι') → ι) i))
            (e.subtypeEquiv (p := fun (j : ι) ↦ j ≠ (e.symm : (a : ι') → ι) i) (q := fun (b : ι') ↦ b ≠ i) sorry) :
          (a : { j : ι' // j ≠ i }) → V)
        j :
      V)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw : HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
  HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₁ : 1 -
    HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
  HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₁ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₂ : 1 -
    HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
  HAdd.hAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₁ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₂ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₃ : 1 -
    HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
  HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₁ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₂ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₃ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₄ : HSub.hSub (β := k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
    (((b.basisOf i).sumCoords : (a : V) → k) v : k) =
  HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
s : Finset ι
i_1 j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
rw :
  HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (v + (q -ᵥ (b : (a : ι) → P) i)) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₁ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₂ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₃ :
  1 -
      HAdd.hAdd (α := k) (β := k) (((b.basisOf i).sumCoords : (a : V) → k) v : k)
        (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k) =
    HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
rw₄ :
  HSub.hSub (β := k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
      (((b.basisOf i).sumCoords : (a : V) → k) v : k) =
    HAdd.hAdd (α := k) (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
⊢ HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) ((v +ᵥ q) -ᵥ (b : (a : ι) → P) i) : k) =
    HVAdd.hVAdd (α := k) ((-(b.basisOf i).sumCoords : (a : V) → k) v : k)
      (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
have rw₅ : HSub.hSub (β := k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
    (((b.basisOf i).sumCoords : (a : V) → k) v : k) =
  HAdd.hAdd (β := k)
    (HSub.hSub (α := k) (β := k) (1 : k) (((b.basisOf i).sumCoords : (a : V) → k) (q -ᵥ (b : (a : ι) → P) i) : k))
    (-((b.basisOf i).sumCoords : (a : V) → k) v : k)
Tactic: rw [vadd_vsub_assoc, map_add, vadd_eq_add, LinearMap.neg_apply, sub_add_eq_sub_sub_swap,
      add_comm, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
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
e : ι ≃ ι'
i : ι'
⊢ (b.reindex e).coord i = b.coord ((e.symm : (a : ι') → ι) i)
have h : ∀ (p : P),
  Eq.{u_5 + 1} (α := k) (((b.reindex e).coord i : (a : P) → k) p : k)
    ((b.coord ((e.symm : (a : ι') → ι) i) : (a : P) → k) p : k)
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
b : AffineBasis ι k P
i j : ι
h : i ≠ j
⊢ 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)
  (({
          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' := sorry } :
        (a : P) → k)
      ((b : (a : ι) → P) j : P) :
    k)
  (0 : k)
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)
⊢ 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) j : 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]