awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
pos :
  ∀ (hj : j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have neg : ∀ (hj : ¬j = j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: by_cases hj : j = j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have pos : ∀ (i' : ιs j),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
Tactic: subst hj
Cleared hypotheses: j', i', hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
have pos : Eq.{u_2 + 1} (α := R)
  (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := sorry,
                map_smul' := sorry } :
              (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
            (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
          Finsupp.{u_5, u_2} (ιs j) R) :
        (a : ιs j) → R)
      i' :
    R)
  ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
      (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
    R)
Tactic: simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
            Finsupp.{u_5, u_2} (ιs j) R) :
          (a : ιs j) → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
      R)
have pos : Eq.{u_2 + 1} (α := R)
  ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
      (Sigma.mk (β := fun (j : η) ↦ ιs j) j i') :
    R)
  (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := sorry,
                map_smul' := sorry } :
              (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
            (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j :
          Finsupp.{u_5, u_2} (ιs j) R) :
        (a : ιs j) → R)
      i' :
    R)
Tactic: symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have neg : Eq.{u_2 + 1} (α := R)
  (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := sorry,
                map_smul' := sorry,
                invFun := fun (f : (i : η) → Finsupp.{u_5, u_2} (ιs i) R) (i : η) ↦
                  ((s i).repr.symm : (a : ιs i →₀ R) → Ms i) (f i),
                left_inv := sorry, right_inv := sorry } :
              (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
            (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j' :
          Finsupp.{u_5, u_2} (ιs j') R) :
        (a : ιs j') → R)
      i' :
    R)
  ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
      (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
    R)
Tactic: simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ Eq.{u_2 + 1} (α := R)
    (((({ toFun := fun (f : (i : η) → Ms i) (i : η) ↦ ((s i).repr : (a : Ms i) → ιs i →₀ R) (f i), map_add' := ⋯,
                  map_smul' := ⋯,
                  invFun := fun (f : (i : η) → Finsupp.{u_5, u_2} (ιs i) R) (i : η) ↦
                    ((s i).repr.symm : (a : ιs i →₀ R) → Ms i) (f i),
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : (j : η) → Ms j) → (i : η) → ιs i →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) j' :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have neg : Eq.{u_2 + 1} (α := R)
  (((((s j').repr : (a : Ms j') → ιs j' →₀ R) (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i) j') :
          Finsupp.{u_5, u_2} (ιs j') R) :
        (a : ιs j') → R)
      i' :
    R)
  ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
      (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
    R)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ Eq.{u_2 + 1} (α := R)
    (((((s j').repr : (a : Ms j') → ιs j' →₀ R) (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i) j') :
            Finsupp.{u_5, u_2} (ιs j') R) :
          (a : ιs j') → R)
        i' :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
have neg : Sigma.mk (β := fun (j : η) ↦ ιs j) j' i' ≠ Sigma.mk (β := fun (j : η) ↦ ιs j) j i
Tactic: rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)
have h : ∀ (j' : η) (i' : ιs j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
h :
  ∀ (j' : η) (i' : ιs j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)
have pos : ∀ (j' : η) (i' : ιs j') (hj : j = j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst : Semiring R
inst_1 : (i : η) → AddCommMonoid (Ms i)
inst_2 : (i : η) → Module.{u_2, u_6} R (Ms i)
inst_3 : Fintype η
inst_4 : DecidableEq η
s : (j : η) → Basis.{u_5, u_2, u_6} (ιs j) R (Ms j)
j : η
i : ιs j
h :
  ∀ (j' : η) (i' : ιs j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
pos :
  ∀ (j' : η) (i' : ιs j') (hj : j = j'),
    Eq.{u_2 + 1} (α := R)
      (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
                (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
              (j : η) × ιs j →₀ R) :
            (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
      ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
          (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
        R)
⊢ Eq (α := (j : η) × ιs j →₀ R)
    (((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
        (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
      (j : η) × ιs j →₀ R)
    (Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (j : η) × ιs j →₀ R)
have neg : ∀ (j' : η) (i' : ιs j') (hj : ¬j = j'),
  Eq.{u_2 + 1} (α := R)
    (((((Pi.basis (ιs := ιs) (Ms := Ms) s).repr : (a : (j : η) → Ms j) → (j : η) × ιs j →₀ R)
              (single (M := Ms) j ((s j : (a : ιs j) → Ms j) i)) :
            (j : η) × ιs j →₀ R) :
          (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
    ((Finsupp.single (Sigma.mk (β := fun (j : η) ↦ ιs j) j i) 1 : (a : (j : η) × ιs j) → R)
        (Sigma.mk (β := fun (j : η) ↦ ιs j) j' i') :
      R)
Tactic: classical
  ext ⟨j', i'⟩
  by_cases hj : j = j'
  · subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]
  simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
    LinearEquiv.piCongrRight]
  dsimp
  rw [Pi.single_eq_of_ne (Ne.symm hj), map_zero, Finsupp.zero_apply,
    Finsupp.single_eq_of_ne]
  rintro ⟨⟩
  contradiction
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have h1 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) 1 : k) (1 : k)
Tactic: have h1 := map_one φ
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
h1 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) 1 : k) (1 : k)
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have have : ∀ (this : Fintype G), ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
Tactic: have := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (hypothesis)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
h1 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) 1 : k) (1 : k)
this : Fintype G
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have h1₁ : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
Tactic: simp only [← Finset.univ_sum_single (1 : G → k), Pi.one_apply, map_sum] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
⊢ ∃ (s : G), Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
have by_contra : ∀ (this : ¬∃ (s : G), Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)),
  False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have obtain : ∀ (s : G) (hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)),
  ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
Tactic: obtain ⟨s, hs⟩ : ∃ (s : G), φ (Pi.single s 1) ≠ 0 := by
    by_contra
    simp_all
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
s : G
hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
⊢ ∀ (t : G), t ≠ s → Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) t 1) : k) (0 : k)
have refine : ∀ (x : G),
  x ≠ s →
    HMul.hMul (α := k) (β := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k)
        ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1) : k) =
      0
Tactic: refine fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
s : G
hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
x : G
h : x ≠ s
⊢ HMul.hMul (α := k) (β := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k)
      ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1) : k) =
    0
have rw : Eq.{u_1 + 1} (α := k)
  ((φ : (a : G → k) → k)
      (HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1)) :
    k)
  (0 : k)
Tactic: rw [← map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
s : G
hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
x : G
h : x ≠ s
⊢ Eq.{u_1 + 1} (α := k)
    ((φ : (a : G → k) → k)
        (HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1)) :
      k)
    (0 : k)
have h : HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) = 0
Tactic: convert! map_zero φ
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
s : G
hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
x : G
h : x ≠ s
⊢ HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) = 0
have h : ∀ (u : G),
  HMul.hMul (α := G → k) (β := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) u =
    0 u
Tactic: ext u
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
Goal:
k : Type u_1
G : Type u_2
inst : CommSemiring k
inst_1 : NoZeroDivisors k
inst_2 : Nontrivial k
inst_3 : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
s : G
hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)
x : G
h : x ≠ s
u : G
⊢ HMul.hMul (α := G → k) (β := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) u =
    0 u
have pos : u = s →
  HMul.hMul (α := G → k) (β := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) u =
    0 u
Tactic: by_cases u = s