awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    (toFun S f (1 ⊗ₜ[R] x))
have h : Eq (α := S ⊗[R] N)
  (1 ⊗ₜ[R]
    Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
      (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
  ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)))
Tactic: convert! f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h :
  Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)))
⊢ Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    (toFun S f (1 ⊗ₜ[R] x))
have h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
Tactic: convert! f.isCompat_apply (Algebra.ofId R S) (1 ⊗ₜ[R] x)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N)
    (1 ⊗ₜ[R]
      Function.comp (β := R ⊗[R] N) (⇑(TensorProduct.lid R N) : (a : R ⊗[R] N) → N)
        (toFun R f ∘ (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M)) x)
    ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)))
have h : Eq (α := S ⊗[R] N)
  ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
  ((rTensor N (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (toFun R f (1 ⊗ₜ[R] x)) : S ⊗[R] N)
Tactic: simp only [Function.comp_apply, TensorProduct.lid_symm_apply, TensorProduct.includeRight_lid]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.ofId R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
Tactic: rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.ofId R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.ofId R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
Tactic: rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.ofId R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.ofId R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) ((rTensor M (toLinearMap (Algebra.ofId R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h₂ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
Tactic: rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] P) (toFun S (g.comp f)) (toFun S g ∘ toFun S f)
have h : ∀ (t : S ⊗[R] M), toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h : ∀ (s : Finset S) (p : MvPolynomial (Fin s.card) R ⊗[R] M)
  (ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t),
  toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
Tactic: obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have hb : π R N S
    (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
      (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
  toFun S f t
Tactic: have hb : PolynomialLaw.π R N S ⟨s, f.toFun' _ p⟩ = f.toFun S t := by
    simp only [toFun_eq_rTensor_φ_toFun' _ ha, π]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
hb :
  π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h : toFun S (g.comp f) t = toFun S g (toFun S f t)
Tactic: rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
hb :
  π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t
h : toFun S (g.comp f) t = toFun S g (toFun S f t)
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h₁ : toFun S (g.comp f) t =
  (rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
    (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
Tactic: rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
hb :
  π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t
h : toFun S (g.comp f) t = toFun S g (toFun S f t)
h₁ :
  toFun S (g.comp f) t =
    (rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h₂ : Eq (α := S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      ((g.comp f).toFun' (MvPolynomial (Fin s.card) R) p) :
    S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
    S ⊗[R] P)
Tactic: rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
hb :
  π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t
h : toFun S (g.comp f) t = toFun S g (toFun S f t)
h₁ :
  toFun S (g.comp f) t =
    (rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
h₂ :
  Eq (α := S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        ((g.comp f).toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
      S ⊗[R] P)
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h₃ : Eq (α := S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      ((g.toFun' (MvPolynomial (Fin s.card) R) ∘ f.toFun' (MvPolynomial (Fin s.card) R)) p) :
    S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
    S ⊗[R] P)
Tactic: rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_5
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst_7 : CommSemiring S
inst_8 : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] M) s p) = t
hb :
  π R N S
      (Sigma.mk (β := fun (s : Finset S) ↦ MvPolynomial (Fin s.card) R ⊗[R] N) s
        (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    toFun S f t
h : toFun S (g.comp f) t = toFun S g (toFun S f t)
h₁ :
  toFun S (g.comp f) t =
    (rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
h₂ :
  Eq (α := S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        ((g.comp f).toFun' (MvPolynomial (Fin s.card) R) p) :
      S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
      S ⊗[R] P)
h₃ :
  Eq (α := S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        ((g.toFun' (MvPolynomial (Fin s.card) R) ∘ f.toFun' (MvPolynomial (Fin s.card) R)) p) :
      S ⊗[R] P)
    ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
        (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
      S ⊗[R] P)
⊢ toFun S (g.comp f) t = (toFun S g ∘ toFun S f) t
have h₄ : Eq (α := S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
    S ⊗[R] P)
  ((rTensor P (toLinearMap (φ R s)) : (a : MvPolynomial (Fin s.card) R ⊗[R] P) → S ⊗[R] P)
      (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) :
    S ⊗[R] P)
Tactic: rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]
-- 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
inst_3 : StrongRankCondition R
pb : PowerBasis R S
⊢ Module.finrank R S = pb.dim
have rw : Fintype.card (Fin pb.dim) = pb.dim
Tactic: rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]
-- 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
inst_3 : StrongRankCondition R
pb : PowerBasis R S
rw : Fintype.card (Fin pb.dim) = pb.dim
⊢ Module.finrank R S = pb.dim
have rw₁ : pb.dim = pb.dim
Tactic: rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]
-- 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 : ℕ
⊢ Eq.{u_2 + 1} (α := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))
    ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ))
have h : ∀ (n : S),
  Membership.mem (γ := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ)) n ↔
    Membership.mem (γ := Set S) ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ)) n
Tactic: ext n
-- 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 : ℕ
n : S
⊢ Membership.mem (γ := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ)) n ↔
    Membership.mem (γ := Set S) ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ)) n
have h : (∃ (y : Fin d), x ^ (↑y : ℕ) = n) ↔ ∃ x_1 < d, x ^ x_1 = n
Tactic: simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
-- 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
x y : S
d : ℕ
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))) y ↔
    ∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f
have this : Eq.{u_2 + 1} (α := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))
  ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ))
Tactic: have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) := by
    ext n
    simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
    exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
-- 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 : ℕ
this :
  Eq.{u_2 + 1} (α := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))
    ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ))
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))) y ↔
    ∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f
have simp : (∃ (l : ℕ →₀ R),
    (∀ (x : ℕ), d ≤ x → Eq (α := R) ((l : (a : ℕ) → R) x : R) (0 : R)) ∧
      ∑ x_1 ∈ l.support, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((l : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) =
        y) ↔
  ∃ (q : AddMonoidAlgebra R ℕ),
    (∀ (m : ℕ), d ≤ m → Eq (α := R) ((q : (a : ℕ) → R) m : R) (0 : R)) ∧
      y =
        ∑ x_1 ∈ { toFinsupp := q : R[X] }.support,
          HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((q : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1)
Tactic: simp only [this, mem_span_image_iff_linearCombination, degree_lt_iff_coeff_zero,
    exists_iff_exists_finsupp, coeff, aeval_def, eval₂_eq_sum, Polynomial.sum,
    mem_supported', linearCombination, Finsupp.sum, Algebra.smul_def,
    LinearMap.id_coe, id, not_lt, Finsupp.coe_lsum, LinearMap.coe_smulRight,
    Finset.mem_range, Finset.mem_coe]
-- 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 : ℕ
this :
  Eq.{u_2 + 1} (α := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))
    ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ))
⊢ (∃ (l : ℕ →₀ R),
      (∀ (x : ℕ), d ≤ x → Eq (α := R) ((l : (a : ℕ) → R) x : R) (0 : R)) ∧
        ∑ x_1 ∈ l.support,
            HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((l : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) =
          y) ↔
    ∃ (q : AddMonoidAlgebra R ℕ),
      (∀ (m : ℕ), d ≤ m → Eq (α := R) ((q : (a : ℕ) → R) m : R) (0 : R)) ∧
        y =
          ∑ x_1 ∈ { toFinsupp := q : R[X] }.support,
            HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((q : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1)
have simp_rw : (∃ (l : ℕ →₀ R),
    (∀ (x : ℕ), d ≤ x → Eq (α := R) ((l : (a : ℕ) → R) x : R) (0 : R)) ∧
      ∑ x_1 ∈ l.support, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((l : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) =
        y) ↔
  ∃ (q : AddMonoidAlgebra R ℕ),
    (∀ (m : ℕ), d ≤ m → Eq (α := R) ((q : (a : ℕ) → R) m : R) (0 : R)) ∧
      ∑ x_1 ∈ { toFinsupp := q : R[X] }.support,
          HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((q : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) =
        y
Tactic: simp_rw [@eq_comm _ 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
x y : S
d : ℕ
hd : d ≠ 0
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))) y ↔
    ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
have rw : (∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f) ↔
  ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
Tactic: rw [mem_span_pow']
-- 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]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f) ↔
    ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
have mp : (∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f) →
  ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
Tactic: constructor
-- 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
mp :
  (∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f) →
    ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
⊢ (∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f) ↔
    ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
have mpr : (∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f) →
  ∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f
Tactic: constructor
-- 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.degree < (↑d : WithBot ℕ)
hy : y = (aeval x : (a : R[X]) → S) f
⊢ ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f
have mp : f.natDegree < d
Tactic: refine ⟨f, ?_, hy⟩
-- 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.degree < (↑d : WithBot ℕ)
hy : y = (aeval x : (a : R[X]) → S) f
⊢ f.natDegree < d
have pos : ∀ (hf : f = 0), f.natDegree < d
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.degree < (↑d : WithBot ℕ)
hy : y = (aeval x : (a : R[X]) → S) f
pos : ∀ (hf : f = 0), f.natDegree < d
⊢ f.natDegree < d
have neg : ∀ (hf : ¬f = 0), f.natDegree < d
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.degree < (↑d : WithBot ℕ)
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
⊢ f.natDegree < d
have pos : ∀ (h : LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)), 0 < d
Tactic: simp only [hf, natDegree_zero, degree_zero] at h ⊢
Cleared hypotheses: 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
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x : (a : R[X]) → S) f
⊢ ∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f
have mpr : f.degree < (↑d : WithBot ℕ)
Tactic: refine ⟨f, ?_, hy⟩
-- 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
⊢ f.degree < (↑d : WithBot ℕ)
have pos : ∀ (hf : f = 0), f.degree < (↑d : WithBot ℕ)
Tactic: by_cases hf : f = 0