awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 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
Tactic: by_cases u = s
-- 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
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 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)
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
-- 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)
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)
have 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)
Tactic: rwa [Fintype.sum_eq_single s h2] at h1
Cleared hypotheses: h1, hs, h2
-- 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
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 h3 : 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
-- 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)
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
have h : φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
Tactic: use s
-- 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)
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
have 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)
Tactic: refine AlgHom.toLinearMap_injective ((Pi.basisFun k G).ext fun t ↦ ?_)
-- 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)
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)
have 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)
Tactic: by_cases t = s
-- 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)
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)
⊢ 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)
have 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)
Tactic: by_cases t = s
-- 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: 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
-- 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)
have have₁ have₂ : ∀ (this : Fintype G), ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have 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
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
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
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
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have 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
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
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
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
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have 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
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
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
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
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have 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
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
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
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
⊢ ∃ (s : G), φ = Pi.evalAlgHom k (fun (i : G) ↦ k) s
have 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
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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
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)
    ((((piEquiv ι R M : (a : ι → M) → (ι → R) →ₗ[R] M) v : (ι → R) →ₗ[R] M) : (a : ι → R) → M) w : M)
    (∑ i : ι, w i • v i : M)
have 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)
Tactic: simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
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
⊢ 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)) ⊤
have 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)) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_piEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.StdBasis (goal)
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)) ⊤
⊢ 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)) ⊤
have rw₁ : Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_piEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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
⊢ motive a
have rcases : ∀ (a : TensorAlgebra R M), motive ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M) a)
Tactic: rcases algHom_surjective _ _ a with ⟨a, rfl⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.SymmetricAlgebra.Basic (goal)
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)
r : R
⊢ motive
    ((algHom R M : (a : TensorAlgebra R M) → SymmetricAlgebra R M)
      ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r))
have algebraMap₁ : motive ((Algebra.algebraMap R (SymmetricAlgebra R M) : (a : R) → SymmetricAlgebra R M) r)
Tactic: rw [AlgHom.commutes]