awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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
⊢ π 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, π]
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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)
h₄ 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

Tactic:
rw [Function.comp_apply, toFun_eq_rTensor_φ_toFun' _ hb, toFun_eq_rTensor_φ_toFun' _ ha,
    comp_toFun', Function.comp_apply]

Premises used: PolynomialLaw.toFun_eq_rTensor_φ_toFun', Function.comp_apply, PolynomialLaw.comp_toFun'
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
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
m : S ⊗[R] M
⊢ toFun S (g.comp f) m = toFun S g (toFun S f m)

Tactic:
simp only [toFun_comp, Function.comp_apply]

Premises used: Function.comp_apply, PolynomialLaw.toFun_comp
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ Eq.{u_2 + 1} (α := (a : Fin pb.dim) → S) (⇑pb.basis : (a : Fin pb.dim) → S) fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)

Tactic:
funext pb.basis_eq_pow

Premises used: PowerBasis.basis_eq_pow, funext
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ Module.Finite R S

Tactic:
.of_basis pb.basis

Premises used: PowerBasis.basis, Module.Finite.of_basis
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B_1 : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B_1
inst_5 : Algebra A B_1
K : Type u_6
inst_6 : Field K
ι : Type u_7
inst_7 : Fintype ι
B : Basis ι R S
x : S
e : ι ≃ Fin (Fintype.card ι)
hx : ∀ (i : ι), (B : (a : ι) → S) i = x ^ (↑((e : (a : ι) → Fin (Fintype.card ι)) i) : ℕ)
i : Fin (Fintype.card ι)
⊢ (B.reindex e : (a : Fin (Fintype.card ι)) → S) i = x ^ (↑i : ℕ)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_7
inst_3 : Fintype ι
B : Basis ι R S
x : S
e : ι ≃ Fin (Fintype.card ι)
hx : ∀ (i : ι), (B : (a : ι) → S) i = x ^ (↑((e : (a : ι) → Fin (Fintype.card ι)) i) : ℕ)
⊢ (B.PowerBasis e hx).gen = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerBasis
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
rw₁ rw₂ : pb.dim = pb.dim
⊢ Module.finrank R S = pb.dim

Tactic:
rw [Module.finrank_eq_card_basis pb.basis, Fintype.card_fin]

Premises used: Fintype.card_fin, Module.finrank_eq_card_basis, PowerBasis.basis
-- Module: Mathlib.RingTheory.PowerBasis
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 : ℕ
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
⊢ Eq.{u_2 + 1} (α := Set S) (Set.range fun (i : Fin d) ↦ x ^ (↑i : ℕ))
    ((fun (i : ℕ) ↦ x ^ i) '' (↑(Finset.range d) : Set ℕ))

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerBasis
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
h : (∃ (y : Fin d), x ^ (↑y : ℕ) = n) ↔ ∃ x_1 < d, x ^ x_1 = n
⊢ 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:
simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]

Premises used: Set.mem_range, Set.mem_image, Finset.mem_range, Finset.mem_coe
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ (∃ (y : Fin d), x ^ (↑y : ℕ) = n) ↔ ∃ x_1 < d, x ^ x_1 = n

Tactic:
⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩

Premises used: _private.0.PowerBasis.mem_span_pow'.match_5, Exists, Fin.mk, Fin.val, And, HPow.hPow, And.intro, LT.lt, Iff.intro, Exists.intro, Eq, _private.0.PowerBasis.mem_span_pow'.match_4
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ (∃ (y : Fin d), x ^ (↑y : ℕ) = n) ↔ ∃ x_1 < d, x ^ x_1 = n

Tactic:
exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ))

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⟩⟩
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ))
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)
⊢ 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

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]

Premises used: LinearMap.id_coe, Polynomial.sum, Finsupp.sum, id, Finset.mem_range, Polynomial.aeval_def, Polynomial.coeff, Finsupp.coe_lsum, not_lt, Polynomial.degree_lt_iff_coeff_zero, Polynomial.exists_iff_exists_finsupp, Algebra.smul_def, LinearMap.coe_smulRight, Finsupp.mem_span_image_iff_linearCombination, Polynomial.eval₂_eq_sum, Finsupp.linearCombination, Finset.mem_coe, Finsupp.mem_supported'
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ))
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
⊢ (∃ (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_rw [@eq_comm _ y]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.PowerBasis
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)) ∧
        ∑ 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:
Iff.rfl

Premises used: Iff.rfl, AddMonoidAlgebra, Polynomial.support
-- Module: Mathlib.RingTheory.PowerBasis
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)) ∧
        ∑ 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:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.PowerBasis
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
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
⊢ 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

Tactic:
rw [mem_span_pow']

Premises used: PowerBasis.mem_span_pow'
-- Module: Mathlib.RingTheory.PowerBasis
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
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
⊢ (∃ (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
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
⟨f, ?_, hy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.PowerBasis
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
mp : f.natDegree < d
⊢ ∃ (f : R[X]), f.natDegree < d ∧ y = (aeval x : (a : R[X]) → S) f

Tactic:
refine ⟨f, ?_, hy⟩
-- Module: Mathlib.RingTheory.PowerBasis
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
neg : ∀ (hf : ¬f = 0), f.natDegree < d
⊢ f.natDegree < d

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.PowerBasis
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
pos : ∀ (h : LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)), 0 < d
⊢ f.natDegree < d

Tactic:
simp only [hf, natDegree_zero, degree_zero] at h ⊢

Premises used: Polynomial.natDegree_zero, Polynomial.degree_zero
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)
⊢ 0 < d

Tactic:
lt_of_le_of_ne (Nat.zero_le d) hd.symm

Premises used: Nat.zero_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)
⊢ 0 < d

Tactic:
exact lt_of_le_of_ne (Nat.zero_le d) hd.symm

Premises used: Nat.zero_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)
⊢ 0 < d

Tactic:
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Premises used: Nat.zero_le, Ne.symm, WithBot.bot_lt_coe, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
simpa [degree_eq_natDegree hf] using h

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.PowerBasis
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

Tactic:
⟨f, ?_, hy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.PowerBasis
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
mpr : f.degree < (↑d : WithBot ℕ)
⊢ ∃ (f : R[X]), f.degree < (↑d : WithBot ℕ) ∧ y = (aeval x : (a : R[X]) → S) f

Tactic:
refine ⟨f, ?_, hy⟩
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ)
neg : ∀ (hf : ¬f = 0), f.degree < (↑d : WithBot ℕ)
⊢ f.degree < (↑d : WithBot ℕ)

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.RingTheory.PowerBasis
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
pos : ∀ (h : 0 < d), LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)
⊢ f.degree < (↑d : WithBot ℕ)

Tactic:
simp only [hf, natDegree_zero, degree_zero] at h ⊢

Premises used: Polynomial.natDegree_zero, Polynomial.degree_zero
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : 0 < d
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)

Tactic:
lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : 0 < d
⊢ ?_mvar.16497 ≤ ?_mvar.16498

Tactic:
(Nat.zero_le d)

Premises used: Nat.zero_le
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : 0 < d
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)

Tactic:
WithBot.bot_lt_coe d

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : 0 < d
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe d

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerBasis
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]
hy : y = (aeval x : (a : R[X]) → S) f
hf : f = 0
h : 0 < d
⊢ LT.lt (α := WithBot ℕ) ⊥ (↑d : WithBot ℕ)

Tactic:
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Premises used: Nat.zero_le, Ne.symm, WithBot.bot_lt_coe, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.PowerBasis
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 ℕ)

Tactic:
simpa [degree_eq_natDegree hf] using h

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
pb : PowerBasis R S
⊢ pb.dim ≠ 0

Tactic:
fun h =>
  not_nonempty_iff.mpr (h.symm ▸ Fin.isEmpty : IsEmpty (Fin pb.dim)) pb.basis.index_nonempty

Premises used: Iff.mpr, Module.Basis.index_nonempty, Eq.rec, PowerBasis.basis, not_nonempty_iff, Fin.isEmpty, Eq.symm, Not
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
pb : PowerBasis R S
⊢ 0 < pb.dim

Tactic:
Nat.pos_of_ne_zero pb.dim_ne_zero

Premises used: Nat.pos_of_ne_zero, PowerBasis.dim_ne_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
pb : PowerBasis R S
y : S
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ))) y

Tactic:
simpa using pb.basis.mem_span y

Premises used: Module.Basis.mem_span, PowerBasis.basis
-- Module: Mathlib.RingTheory.PowerBasis
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
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.PowerBasis
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
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
⊢ ∃ (f : R[X]), y = (aeval pb.gen : (a : R[X]) → S) f

Tactic:
obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y

Premises used: PowerBasis.exists_eq_aeval
-- Module: Mathlib.RingTheory.PowerBasis
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]
left : 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:
⟨f, hf⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.PowerBasis
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]
left : 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:
exact ⟨f, hf⟩
-- Module: Mathlib.RingTheory.PowerBasis
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')
H : ∀ (x : S), Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') x : S') ((g : (a : S) → S') x : S')
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.RingTheory.PowerBasis
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
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')
⊢ Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') x : S') ((g : (a : S) → S') x : S')

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Premises used: PowerBasis.exists_eq_aeval', rfl