awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x : (a : R[X]) → S) f
pos : ∀ (hf : f = 0), f.degree < (↑d : WithBot ℕ)
⊢ f.degree < (↑d : WithBot ℕ)
have neg : ∀ (hf : ¬f = 0), f.degree < (↑d : WithBot ℕ)
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
⊢ f.degree < (↑d : WithBot ℕ)
have pos : ∀ (h : 0 < d), LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)
Tactic: simp only [hf, natDegree_zero, degree_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
y : S
⊢ ∃ (f : R[X]), y = (aeval pb.gen : (a : R[X]) → S) f
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
y : S
h : Nontrivial S
⊢ ∃ (f : R[X]), y = (aeval pb.gen : (a : R[X]) → S) f
have obtain : ∀ (f : R[X]),
  f.natDegree < pb.dim →
    ∀ (hf : y = (aeval pb.gen : (a : R[X]) → S) f), ∃ (f : R[X]), y = (aeval pb.gen : (a : R[X]) → S) f
Tactic: obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
⊢ f = g
have H : ∀ (x : S), Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') x : S') ((g : (a : S) → S') x : S')
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
x : S
⊢ Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') x : S') ((g : (a : S) → S') x : S')
have H : ∀ (f_1 : R[X]),
  Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f_1 : S) : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f_1 : S) : S')
Tactic: obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f_1 g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
f : R[X]
⊢ Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
have H : Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
  ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
Tactic: rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f_1 g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
f : R[X]
H :
  Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
⊢ Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
have H₁ : Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
  (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
Tactic: rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f_1 g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
f : R[X]
H :
  Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
H₁ :
  Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
⊢ Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
have H₂ : Eq.{u_7 + 1} (α := S') (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
  (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
Tactic: rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
have inl : Subsingleton B → ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
Tactic: rcases subsingleton_or_nontrivial B
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
inl : Subsingleton B → ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
have inr : Nontrivial B → ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
Tactic: rcases subsingleton_or_nontrivial B
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Subsingleton B
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) 0)
have rw : Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk b)
  (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0))
Tactic: rw [SModEq, Subsingleton.eq_zero b, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Subsingleton B
rw :
  Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk b)
    (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0))
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) 0)
have rw₁ : Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
  (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
  (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0) :
    HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
Tactic: rw [SModEq, Subsingleton.eq_zero b, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Subsingleton B
rw :
  Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk b)
    (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0))
rw₁ :
  Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) 0)
have rw₂ : Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk 0)
  (Submodule.Quotient.mk 0)
Tactic: rw [SModEq, Subsingleton.eq_zero b, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
have inr : SModEq (R := B) (Ideal.span {pb.gen}) b
  ((algebraMap A B : (a : A) → B)
    ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) (⟨0, sorry⟩ : Fin pb.dim) :
      A))
Tactic: refine ⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, ⋯⟩ : Fin pb.dim) :
        A))
have H : ∑ i : Fin pb.dim,
    HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
      ((pb.basis : (a : Fin pb.dim) → B) i : B) =
  b
Tactic: have H := pb.basis.sum_repr b
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (hypothesis)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  ∑ i : Fin pb.dim,
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
        ((pb.basis : (a : Fin pb.dim) → B) i : B) =
    b
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, ⋯⟩ : Fin pb.dim) :
        A))
have H₁ : HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, sorry⟩ : Fin pb.dim) :
        A)
      ((pb.basis : (a : Fin pb.dim) → B) (⟨0, sorry⟩ : Fin pb.dim) : B) +
    ∑ x ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((pb.basis : (a : Fin pb.dim) → B) x : B) =
  b
Tactic: rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (notMem_erase _ _)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, ⋯⟩ : Fin pb.dim) :
        A))
have inr : Submodule.Quotient.mk b =
  HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
    HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
        ((algebraMap A B : (a : A) → B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, sorry⟩ : Fin pb.dim) :
            A)) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
Tactic: rw [SModEq, ← add_zero (algebraMap _ _ _), Quotient.mk_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Submodule.Quotient.mk b =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
have inr : Submodule.Quotient.mk
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, sorry⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, sorry⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B)) =
  HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
    HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
        ((algebraMap A B : (a : A) → B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, sorry⟩ : Fin pb.dim) :
            A)) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
Tactic: nth_rewrite 1 [← H]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
        (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, ⋯⟩ : Fin pb.dim) :
            A)
          ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
      (Submodule.Quotient.mk
        (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
          HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
            ((pb.basis : (a : Fin pb.dim) → B) x : B))) =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
have inr : Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
  (Submodule.Quotient.mk
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, sorry⟩ : Fin pb.dim) :
        A)
      ((pb.basis : (a : Fin pb.dim) → B) (⟨0, sorry⟩ : Fin pb.dim) : B)))
  (Submodule.Quotient.mk
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, sorry⟩ : Fin pb.dim) :
        A)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
    (Submodule.Quotient.mk
      ((algebraMap A B : (a : A) → B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)))
⊢ HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
        (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, ⋯⟩ : Fin pb.dim) :
            A)
          ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
      (Submodule.Quotient.mk
        (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
          HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
            ((pb.basis : (a : Fin pb.dim) → B) x : B))) =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
have inr₁ : Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
  (Submodule.Quotient.mk
    (∑ x ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((pb.basis : (a : Fin pb.dim) → B) x : B)))
  (Submodule.Quotient.mk 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B)))
    (Submodule.Quotient.mk 0)
have inr : Membership.mem (γ := Submodule B B) (Ideal.span {pb.gen})
  (∑ x ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim),
    HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) x))
Tactic: rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]
-- Lean 4 proof step from Mathlib.RingTheory.PowerBasis (goal)
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Membership.mem (γ := Submodule B B) (Ideal.span {pb.gen})
    (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) x))
have inr : ∀ (i : Fin pb.dim) (hi : i ∈ Finset.erase univ (⟨0, sorry⟩ : Fin pb.dim)),
  Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i))
Tactic: refine sum_mem _ (fun i hi ↦ ?_)