awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M_1
inst_6 : Module R_1 N_1
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
R : Type u_5
M : Type u_6
N : Type u_7
inst_9 : CommRing R
inst_10 : AddCommGroup M
inst_11 : Module R M
inst_12 : Module.Invertible R M
inst_13 : AddCommGroup N
inst_14 : Module R N
inst_15 : Module.Invertible R N
inst_16 : IsDomain R
⊢ ∃ (I : Ideal R), Nonempty (M ≃ₗ[R] ↥I)

Tactic:
Module.Invertible.exists_linearEquiv_ideal R M

Premises used: Module.Invertible.exists_linearEquiv_ideal
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R_1 : Type u
M_1 : Type v
N_1 : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst : CommSemiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : AddCommMonoid N_1
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R_1 M_1
inst_6 : Module R_1 N_1
inst_7 : Module R_1 P
inst_8 : Module R_1 Q
R : Type u_5
M : Type u_6
N : Type u_7
inst_9 : CommRing R
inst_10 : AddCommGroup M
inst_11 : Module R M
inst_12 : Module.Invertible R M
inst_13 : AddCommGroup N
inst_14 : Module R N
inst_15 : Module.Invertible R N
inst_16 : IsNoetherianRing R
⊢ ∃ (I : Ideal R), Nonempty (M ≃ₗ[R] ↥I)

Tactic:
Module.Invertible.exists_linearEquiv_ideal R M

Premises used: Module.Invertible.exists_linearEquiv_ideal
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
have : ∀ (e : ↥I ⊗[R] ↥J ≃ₗ[R] R), I = ⊤ ∧ J = ⊤
⊢ I = ⊤ ∧ J = ⊤

Tactic:
have ⟨e⟩ := mk_eq_one_iff.mp h
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e : ↥I ⊗[R] ↥J ≃ₗ[R] R
have : ∀ (e : R ≃ₗ[R] ↥(I * J)), I = ⊤ ∧ J = ⊤
⊢ I = ⊤ ∧ J = ⊤

Tactic:
have e := e.symm ≪≫ₗ Submodule.LinearDisjoint.mulMap
    (.of_left_le_one_of_flat I J <| le_top.trans one_eq_top.ge)
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ Function.Injective (α := R) (β := R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)))

Tactic:
Subtype.val_injective.comp e.injective

Premises used: Subtype.val_injective, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
h₁ :
  ∀ (x : R),
    x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
      Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
⊢ Function.Injective (β := R) fun (x : R) ↦ x * (↑((e : (a : R) → ↥(I * J)) 1) : R)

Tactic:
convert! Subtype.val_injective.comp e.injective using 2

Premises used: Subtype.val_injective, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x : R
h₁ :
  HSMul.hSMul (β := R) x (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₂ :
  (↑(HSMul.hSMul (β := ↥(I * J)) x ((e : (a : R) → ↥(I * J)) 1)) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x
h₃ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (HSMul.hSMul (β := R) x 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₄ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) (x * 1)) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₅ :
  Eq (α := R) (↑((e : (a : R) → ↥(I * J)) x) : R)
    (Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x)
h₆ h₇ : Eq.{u_5 + 1} (α := R) (↑((e : (a : R) → ↥(I * J)) x) : R) (↑((e : (a : R) → ↥(I * J)) x) : R)
⊢ x * (↑((e : (a : R) → ↥(I * J)) 1) : R) =
    Function.comp (β := ↥(I * J)) (Subtype.val (p := fun (x : R) ↦ x ∈ I * J)) (⇑e : (a : R) → ↥(I * J)) x

Tactic:
rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]

Premises used: Submodule.coe_smul, Function.comp_apply, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)

Tactic:
have : IsUnit (e 1 : R) := IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› <|
      IsRegular.mem_nonZeroDivisors <| isRightRegular_iff_isRegular.mp <| by
    rw [IsRightRegular]
    convert! Subtype.val_injective.comp e.injective using 2
    rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
left : I = ⊤
right : J = ⊤
⊢ I = ⊤ ∧ J = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ I = ⊤

Tactic:
eq_top_of_isUnit_mem _ ?_ this

Premises used: Ideal.eq_top_of_isUnit_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
left : (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ I
⊢ I = ⊤

Tactic:
refine eq_top_of_isUnit_mem _ ?_ this

Premises used: Ideal.eq_top_of_isUnit_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ J = ⊤

Tactic:
eq_top_of_isUnit_mem _ ?_ this

Premises used: Ideal.eq_top_of_isUnit_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
right : (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ J
⊢ J = ⊤

Tactic:
refine eq_top_of_isUnit_mem _ ?_ this

Premises used: Ideal.eq_top_of_isUnit_mem
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ I

Tactic:
mul_le_right (e 1).2

Premises used: Ideal.mul_le_right, Set.Mem, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ J

Tactic:
mul_le_left (e 1).2

Premises used: Set.Mem, Ideal.mul_le_left, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.PicardGroup
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsFractionRing R R
I J : Ideal R
inst_2 : Module.Invertible R ↥I
inst_3 : Module.Invertible R ↥J
h : Eq (α := Pic R) (Pic.mk R (↥I ⊗[R] ↥J)) 1
e_1 : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
this : IsUnit (M := R) (↑((e : (a : R) → ↥(I * J)) 1) : R)
⊢ (↑((e : (a : R) → ↥(I * J)) 1) : R) ∈ I

Tactic:
exacts [mul_le_right (e 1).2, mul_le_left (e 1).2]

Premises used: Ideal.mul_le_right, Ideal.mul_le_left, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h_1 : CharP R p
h : ∀ (x : ℕ), Eq.{u + 1} (α := R) (↑x : R) 0 ↔ p ∣ x
n : ℕ
rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) 0 ↔ p ∣ n
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0) ↔ p ∣ n
rw₂ : Eq.{u + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
rw₃ rw₄ : p ∣ n ↔ p ∣ n
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n

Tactic:
rw [← map_natCast C, ← C_0, C_inj, h]

Premises used: Polynomial.C, Polynomial.C_inj, Polynomial.C_0, map_natCast
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
h : ExpChar R p
zero : ∀ [CharZero R], ExpChar.{u} R[X] 1
prime : Nat.Prime p → ∀ [CharP R p], ExpChar.{u} R[X] p
⊢ ExpChar.{u} R[X] p

Tactic:
cases h
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : CharZero R
⊢ ExpChar.{u} R[X] 1

Tactic:
ExpChar.zero

Premises used: ExpChar.zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
p : ℕ
hprime : Nat.Prime p
hchar : CharP R p
⊢ ExpChar.{u} R[X] p

Tactic:
ExpChar.prime ‹_›

Premises used: ExpChar.prime
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : Semiring R
inst_1 : CharZero R
⊢ ExpChar.{u} R[X] 1

Tactic:
exacts [ExpChar.zero, ExpChar.prime ‹_›]

Premises used: ExpChar.zero, ExpChar.prime
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : WithBot ℕ
f : R[X]
simp :
  (∀ (i : ℕ) (i_1 : (↑i : WithBot ℕ) > n), Eq (α := R) ((lcoeff R i : (a : R[X]) → R) f : R) (0 : R)) ↔
    ∀ (m : ℕ), n < (↑m : WithBot ℕ) → f.coeff m = 0
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLE R n) f ↔ f.degree ≤ n

Tactic:
simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]

Premises used: Submodule.mem_iInf, Polynomial.degreeLE, LinearMap.mem_ker, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ) (i_1 : (↑i : WithBot ℕ) > n), Eq (α := R) ((lcoeff R i : (a : R[X]) → R) f : R) (0 : R)) ↔
    ∀ (m : ℕ), n < (↑m : WithBot ℕ) → f.coeff m = 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
m n : WithBot ℕ
H : m ≤ n
⊢ LE.le (α := Submodule R R[X]) (degreeLE R m) (degreeLE R n)

Tactic:
fun _ hf =>
  mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) H)

Premises used: Iff.mpr, Iff.mp, Polynomial.mem_degreeLE, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a :
  degreeLE R (↑n : WithBot ℕ) ≤
    Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])
a₁ :
  Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]) ≤
    degreeLE R (↑n : WithBot ℕ)
⊢ degreeLE R (↑n : WithBot ℕ) =
    Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLE R (↑n : WithBot ℕ)) p
⊢ p.degree ≤ (↑n : WithBot ℕ)

Tactic:
replace hp := mem_degreeLE.1 hp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
a :
  Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X])) p

Tactic:
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))

Tactic:
Submodule.sum_mem _ fun k hk => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
a :
  ∀ (k : ℕ) (hk : k ∈ p.support),
    Membership.mem (α := R[X]) (γ := Submodule R R[X])
      (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
      ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))

Tactic:
refine Submodule.sum_mem _ fun k hk => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
⊢ k ≤ (↑n : ℕ)

Tactic:
have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k ≤ (↑n : ℕ)
a :
  Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (p.coeff k • HPow.hPow (α := R[X]) X k)
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])

Tactic:
rw [← C_mul_X_pow_eq_monomial, C_mul']

Premises used: Polynomial.C_mul', Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k ≤ (↑n : ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (p.coeff k • HPow.hPow (α := R[X]) X k)

Tactic:
Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)

Premises used: Iff.mpr, Finset.mem_image, Set.Mem, Nat.lt_succ_of_le, Finset.mem_range, And.intro, Exists.intro, Submodule.subset_span, Finset.mem_coe, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k ≤ (↑n : ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]))
    (p.coeff k • HPow.hPow (α := R[X]) X k)

Tactic:
refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)

Premises used: Iff.mpr, Finset.mem_image, Nat.lt_succ_of_le, Finset.mem_range, And.intro, Exists.intro, Submodule.subset_span, Finset.mem_coe, rfl, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a :
  (↑(range (n + 1)) : Set ℕ) ⊆ (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLE R (↑n : WithBot ℕ)) : Set R[X])
⊢ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range (n + 1))) : Set R[X]) ≤
    degreeLE R (↑n : WithBot ℕ)

Tactic:
rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]

Premises used: Finset.coe_image, Set.image_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range (n + 1)) : Set ℕ)
a : degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) ≤ (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Set ℕ)
    ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) ⁻¹' (↑(degreeLE R (↑n : WithBot ℕ)) : Set R[X])) k

Tactic:
apply mem_degreeLE.2

Premises used: Iff.mpr, Polynomial.mem_degreeLE
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range (n + 1)) : Set ℕ)
⊢ degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) ≤ (↑n : WithBot ℕ)

Tactic:
(degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)

Premises used: Iff.mpr, Polynomial.degree_X_pow_le, Finset.mem_range, WithBot.coe_le_coe, Nat.le_of_lt_succ, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n k : ℕ
hk : k ∈ (↑(range (n + 1)) : Set ℕ)
⊢ degree.{u} (R := R) ((fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) k) ≤ (↑n : WithBot ℕ)

Tactic:
exact
    (degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)

Premises used: Iff.mpr, Polynomial.degree_X_pow_le, Finset.mem_range, WithBot.coe_le_coe, Nat.le_of_lt_succ, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
f : R[X]
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R n) f ↔ f.degree < (↑n : WithBot ℕ)

Tactic:
simpa [degreeLT, Submodule.mem_iInf] using (degree_lt_iff_coeff_zero _ _).symm

Premises used: Polynomial.degreeLT, Submodule.mem_iInf, Polynomial.degree_lt_iff_coeff_zero, Iff.symm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
m n : ℕ
H : m ≤ n
⊢ LE.le (α := Submodule R R[X]) (degreeLT R m) (degreeLT R n)

Tactic:
fun _ hf =>
  mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 H)

Premises used: Iff.mpr, WithBot.coe_le_coe, Iff.mp, Polynomial.mem_degreeLT, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
a : degreeLT R n ≤ Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])
a₁ : Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]) ≤ degreeLT R n
⊢ degreeLT R n = Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : Membership.mem (γ := Submodule R R[X]) (degreeLT R n) p
⊢ p.degree < (↑n : WithBot ℕ)

Tactic:
replace hp := mem_degreeLT.1 hp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
a :
  Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])) p

Tactic:
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))

Tactic:
Submodule.sum_mem _ fun k hk => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
a :
  ∀ (k : ℕ) (hk : k ∈ p.support),
    Membership.mem (α := R[X]) (γ := Submodule R R[X])
      (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
      ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (∑ n ∈ p.support, (monomial n : (a : R) → R[X]) (p.coeff n))

Tactic:
refine Submodule.sum_mem _ fun k hk => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
⊢ k < n

Tactic:
have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k < n
a :
  Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (p.coeff k • HPow.hPow (α := R[X]) X k)
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    ((monomial k : (a : R) → R[X]) (p.coeff k) : R[X])

Tactic:
rw [← C_mul_X_pow_eq_monomial, C_mul']

Premises used: Polynomial.C_mul', Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ HPow.hPow (α := R[X]) X k ∈ (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X])

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < (↑n : WithBot ℕ)
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ Membership.mem (γ := Submodule R R[X])
    (Submodule.span R (↑(image (fun (n : ℕ) ↦ HPow.hPow (α := R[X]) X n) (range n)) : Set R[X]))
    (p.coeff k • HPow.hPow (α := R[X]) X k)

Tactic:
refine Submodule.smul_mem _ _ (Submodule.subset_span <| by grind)

Premises used: Submodule.subset_span, Submodule.smul_mem