-- 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 have₁ have₂ : ∀ (this : Fintype G), ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have₃ :
  ∀ (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₄ :
  ∀ (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)),
    ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have₅ :
  ∀ (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)),
    ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have₆ :
  ∀ (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)),
    ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
h :
  ∀ (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
h₁ :
  ∀ (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),
    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)
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s

Tactic:
classical
  have := Fintype.ofFinite G
  simp only [← Finset.univ_sum_single (1 : G → k), Pi.one_apply, map_sum] at h1
  obtain ⟨s, hs⟩ : ∃ (s : G), φ (Pi.single s 1) ≠ 0 := by
    by_contra
    simp_all
  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
  have h3 : φ (Pi.single s 1) = 1 := by
    rwa [Fintype.sum_eq_single s h2] at h1
  use s
  refine AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)
  by_cases t = s <;> simp_all

Premises used: Pi.one_apply, AlgHom.toLinearMap_injective, map_sum, Pi.basisFun, Module.Basis.ext