awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
inst : Semiring R
inst_1 : Finite η
inst_2 : DecidableEq η
i : η
⊢ Eq (α := η → R) ((basisFun R η : (a : η) → η → R) i : η → R) (single (M := fun (j : η) ↦ R) i 1 : (j : η) → R)

Tactic:
simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply]

Premises used: LinearEquiv.refl_symm, LinearEquiv.refl_apply, Pi.basisFun, Module.Basis.coe_ofEquivFun
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
inst : Semiring R
inst_1 : Finite η
x : η → R
i : η
⊢ (((Basis.repr (basisFun R η) : (a : η → R) → η →₀ R) x : η →₀ R) : (a : η) → R) i = x i

Tactic:
simp [basisFun]

Premises used: Pi.basisFun
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
inst : Semiring R
inst_1 : Finite η
⊢ Eq (α := (η → R) ≃ₗ[R] η → R) (Basis.equivFun (basisFun R η)) (LinearEquiv.refl R (η → R))

Tactic:
Basis.equivFun_ofEquivFun _

Premises used: Module.Basis.equivFun_ofEquivFun, Pi.basisFun
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
R : Type u_2
η : Type u_4
inst : Semiring R
inst_1 : Finite η
s : Set η
v : η → R
⊢ Membership.mem (γ := Submodule R (η → R)) (spanSubset R s) v ↔ ∀ i ∉ s, v i = 0

Tactic:
simp [spanSubset, Module.Basis.mem_span_image, Finsupp.support_subset_iff]

Premises used: Module.Basis.mem_span_image, Finsupp.support_subset_iff, Pi.spanSubset
-- Module: Mathlib.LinearAlgebra.StdBasis
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
⊢ Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) 1 : k) (1 : k)

Tactic:
have h1 := map_one φ
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
have : ∀ (this : Fintype G), ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s

Tactic:
have := Fintype.ofFinite G
-- Module: Mathlib.LinearAlgebra.StdBasis
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
⊢ 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

Premises used: Finset.univ_sum_single, Pi.one_apply, map_sum, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.StdBasis
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
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
⊢ ∃ (s : G), Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k)

Tactic:
by_contra
-- Module: Mathlib.LinearAlgebra.StdBasis
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_1 : Fintype G
h1 : Eq.{u_1 + 1} (α := k) (∑ x : G, (φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) x 1)) 1
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:
simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
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
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
⊢ ∃ (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
-- Module: Mathlib.LinearAlgebra.StdBasis
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)

Tactic:
fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs

Premises used: Or.resolve_left, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
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
⊢ ∀ (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)

Tactic:
refine fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs

Premises used: Or.resolve_left, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.LinearAlgebra.StdBasis
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
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)
⊢ 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:
rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.LinearAlgebra.StdBasis
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) 0 : k) (0 : k)

Tactic:
map_zero φ

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.StdBasis
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_1 : x ≠ s
h : HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) = 0
⊢ 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:
convert! map_zero φ

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.StdBasis
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_1 : x ≠ s
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
⊢ HMul.hMul (α := G → k) (Pi.single (M := fun (a : G) ↦ k) s 1) (Pi.single (M := fun (a : G) ↦ k) x 1) = 0

Tactic:
ext u
-- Module: Mathlib.LinearAlgebra.StdBasis
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
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
neg :
  ¬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
⊢ 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
-- Module: Mathlib.LinearAlgebra.StdBasis
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
h_1 : 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:
simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
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
h_1 : ¬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:
simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
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)

Tactic:
have h2 : ∀ t ≠ s, φ (Pi.single t 1) = 0 := by
    refine fun _ _ ↦ (eq_zero_or_eq_zero_of_mul_eq_zero ?_).resolve_left hs
    rw [← map_mul]
    convert! map_zero φ
    ext u
    by_cases u = s <;> simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h1 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k))
    (hs : Ne.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (0 : k))
    (h2 :
      ∀ (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)),
    Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
⊢ Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)

Tactic:
rwa [Fintype.sum_eq_single s h2] at h1

Premises used: Fintype.sum_eq_single
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
⊢ Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)

Tactic:
have h3 : φ (Pi.single s 1) = 1 := by
    rwa [Fintype.sum_eq_single s h2] at h1
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
h : φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s

Tactic:
use s
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
⊢ φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s

Tactic:
AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)

Premises used: AlgHom.toLinearMap_injective, Pi.basisFun, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
h :
  ∀ (t : G),
    Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
      ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
          ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
        k)
⊢ φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s

Tactic:
refine AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)

Premises used: AlgHom.toLinearMap_injective, Pi.basisFun, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
t : G
pos :
  t = s →
    Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
      ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
          ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
        k)
neg :
  ¬t = s →
    Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
      ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
          ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
        k)
⊢ Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
    ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
        ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
      k)

Tactic:
by_cases t = s
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
t : G
h : t = s
⊢ Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
    ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
        ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
      k)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
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)
h2 : ∀ (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)
h3 : Eq.{u_1 + 1} (α := k) ((φ : (a : G → k) → k) (Pi.single (M := fun (a : G) ↦ k) s 1) : k) (1 : k)
t : G
h : ¬t = s
⊢ Eq.{u_1 + 1} (α := k) ((φ.toLinearMap : (a : G → k) → k) ((Pi.basisFun k G : (a : G) → G → k) t : G → k) : k)
    ((toLinearMap (Pi.evalAlgHom k (fun (i : G) ↦ k) s) : (a : G → k) → k)
        ((Pi.basisFun k G : (a : G) → G → k) t : G → k) :
      k)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_5
R : Type u_6
M : Type u_7
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
w : ι → R
simp :
  Eq.{u_7 + 1} (α := M)
    (∑ x : ι,
      HSMul.hSMul.{u_6, u_7, u_7} (α := R)
        ((((Basis.repr (Pi.basisFun R ι) : (a : ι → R) → ι →₀ R) w : ι →₀ R) : (a : ι) → R) x : R) (v x))
    (∑ i : ι, w i • v i)
⊢ Eq.{u_7 + 1} (α := M)
    ((((piEquiv ι R M : (a : ι → M) → (ι → R) →ₗ[R] M) v : (ι → R) →ₗ[R] M) : (a : ι → R) → M) w : M)
    (∑ i : ι, w i • v i : M)

Tactic:
simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]

Premises used: Module.Basis.constr_apply_fintype, Module.piEquiv, Module.Basis.equivFun_apply
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_5
R : Type u_6
M : Type u_7
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
w : ι → R
⊢ Eq.{u_7 + 1} (α := M)
    (∑ x : ι,
      HSMul.hSMul.{u_6, u_7, u_7} (α := R)
        ((((Basis.repr (Pi.basisFun R ι) : (a : ι → R) → ι →₀ R) w : ι →₀ R) : (a : ι) → R) x : R) (v x))
    (∑ i : ι, w i • v i)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
⊢ Eq (α := Submodule R M)
    (LinearMap.range (R := R) (M := ι → R) (τ₁₂ := RingHom.id R) ((piEquiv ι R M : (a : ι → M) → (ι → R) →ₗ[R] M) v))
    (span R (Set.range v))

Tactic:
Basis.constr_range _ _

Premises used: Module.Basis.constr_range
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Finite ι
inst_1 : CommSemiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
rw :
  Eq.{u_3 + 1} (α := Submodule R M)
      (LinearMap.range (R := R) (M := ι → R) (τ₁₂ := RingHom.id R) ((piEquiv ι R M : (a : ι → M) → (ι → R) →ₗ[R] M) v))
      ⊤ ↔
    Eq (α := Submodule R M) (span R (Set.range v)) ⊤
rw₁ rw₂ : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
⊢ Surjective (α := ι → R) (β := M)
      (⇑((piEquiv ι R M : (a : ι → M) → (ι → R) →ₗ[R] M) v : (ι → R) →ₗ[R] M) : (a : ι → R) → M) ↔
    Eq (α := Submodule R M) (span R (Set.range v)) ⊤

Tactic:
rw [← LinearMap.range_eq_top, range_piEquiv]

Premises used: Module.range_piEquiv, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M_1 : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
M : ι → Type u_4
inst_3 : Finite ι
inst_4 : (i : ι) → AddCommMonoid (M i)
inst_5 : (i : ι) → Module.{u_2, u_4} R (M i)
inst_6 : ∀ (i : ι), Free.{u_2, u_4} R (M i)
⊢ Free R ((i : ι) → M i)

Tactic:
let ⟨_⟩ := nonempty_fintype ι
  .of_basis <| Pi.basis fun i => Module.Free.chooseBasis R (M i)

Premises used: Pi.basis, Module.Free, nonempty_fintype, Module.Free.of_basis, _private.0.Module.Free.pi.match_1, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
inst_4 : Free R M
⊢ Free R (ι → M)

Tactic:
Free.pi _ _

Premises used: Module.Free.pi
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Function.Surjective (α := TensorAlgebra R M) (β := SymmetricAlgebra R M)
    (⇑(algHom R M) : (a : TensorAlgebra R M) → SymmetricAlgebra R M)

Tactic:
RingQuot.mkAlgHom_surjective _ _

Premises used: RingQuot.mkAlgHom_surjective
-- Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
motive : SymmetricAlgebra R M → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
ι : ∀ (x : M), motive ((SymmetricAlgebra.ι R M : (a : M) → SymmetricAlgebra R M) x)
mul : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)
add : ∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)
a : SymmetricAlgebra R M
rcases : ∀ (a : TensorAlgebra R M), motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
⊢ motive a

Tactic:
rcases algHom_surjective _ _ a with ⟨a, rfl⟩

Premises used: SymmetricAlgebra.algHom_surjective, rfl