awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
h : Ne.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
inr :
  degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) =
    degree.{v} (R := S) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a))
⊢ ∃ (q : R[X]),
    map f q = (monomial n : (a : S) → S[X]) ((f : (a : R) → S) a) ∧
      q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a))

Tactic:
refine ⟨monomial n a, map_monomial f, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
h : Ne.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
inr : a ≠ 0
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) =
    degree.{v} (R := S) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a))

Tactic:
rw [degree_monomial, degree_monomial n h]

Premises used: Polynomial.degree_monomial
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
h : Ne.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ a ≠ 0

Tactic:
mt (fun ha ↦ ha ▸ map_zero f) h

Premises used: mt
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
a : R
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X])
h : Ne.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ a ≠ 0

Tactic:
exact mt (fun ha ↦ ha ▸ map_zero f) h

Premises used: mt
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
⊢ ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
rw [lifts_iff_coeff_lifts] at hlifts

Premises used: Polynomial.lifts_iff_coeff_lifts
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
⊢ ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k

Tactic:
have hg : ∀ k, f (g k) = p.coeff k := fun k ↦ (hlifts k).choose_spec
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
simp_rw : map f (∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)) = p
simp_rw₁ : ∑ i ∈ p.support, map f ((monomial i : (a : R) → R[X]) (g i)) = p
simp_rw₂ : ∑ x ∈ p.support, (monomial x : (a : S) → S[X]) ((f : (a : R) → S) (g x)) = p
simp_rw₃ : ∑ x ∈ p.support, (monomial x : (a : S) → S[X]) (p.coeff x) = p
⊢ map f q = p

Tactic:
simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]

Premises used: Polynomial.map_monomial, Polynomial.map_sum, Polynomial.as_sum_support
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
⊢ map f q = p

Tactic:
have hq : map f q = p := by simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
simp_rw : ∀ (a : ℕ), g a = 0 → p.coeff a = 0
⊢ q.support = p.support

Tactic:
simp_rw [Finset.ext_iff, mem_support_iff, q, finsetSum_coeff, coeff_monomial,
      Finset.sum_ite_eq', ite_ne_right_iff, mem_support_iff, and_iff_left_iff_imp, not_imp_not]

Premises used: Finset.sum_ite_eq', Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Finset.ext_iff, Polynomial.coeff_monomial, ite_ne_right_iff, and_iff_left_iff_imp, not_imp_not
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
k : ℕ
h : g k = 0
rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g k) : S) (0 : S)
rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
rw₂ rw₃ : Eq.{v + 1} (α := S) 0 0
⊢ p.coeff k = 0

Tactic:
rw [← hg, h, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
⊢ ∀ (a : ℕ), g a = 0 → p.coeff a = 0

Tactic:
exact fun k h ↦ by rw [← hg, h, map_zero]
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
⊢ q.support = p.support

Tactic:
have hq' : q.support = p.support := by
    simp_rw [Finset.ext_iff, mem_support_iff, q, finsetSum_coeff, coeff_monomial,
      Finset.sum_ite_eq', ite_ne_right_iff, mem_support_iff, and_iff_left_iff_imp, not_imp_not]
    exact fun k h ↦ by rw [← hg, h, map_zero]
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
hq' : q.support = p.support
⊢ ∃ (q : R[X]), map f q = p ∧ q.support = p.support

Tactic:
⟨q, hq, hq'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k : (a : R) → R[X]) (g k)
hq : map f q = p
hq' : q.support = p.support
⊢ ∃ (q : R[X]), map f q = p ∧ q.support = p.support

Tactic:
exact ⟨q, hq, hq'⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
obtain : ∀ (q : R[X]) (hq : map f q = p) (hq' : q.support = p.support), ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree

Tactic:
obtain ⟨q, hq, hq'⟩ := exists_support_eq_of_mem_lifts hlifts

Premises used: Polynomial.exists_support_eq_of_mem_lifts
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
q : R[X]
hq : map f q = p
hq' : q.support = p.support
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree

Tactic:
⟨q, hq, congrArg Finset.max hq'⟩

Premises used: congrArg, And.intro, Exists.intro, Finset.max
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
q : R[X]
hq : map f q = p
hq' : q.support = p.support
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree

Tactic:
exact ⟨q, hq, congrArg Finset.max hq'⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
rw [lifts_iff_coeff_lifts] at hlifts

Premises used: Polynomial.lifts_iff_coeff_lifts
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hlifts₁ : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
⊢ p.Monic

Tactic:
rw [lifts_iff_coeff_lifts] at hlifts

Premises used: Polynomial.lifts_iff_coeff_lifts
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
⊢ ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k

Tactic:
have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
simp_rw :
  map f
      (HPow.hPow (α := R[X]) X p.natDegree +
        ∑ k ∈ Finset.range p.natDegree,
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)) =
    p
simp_rw₁ :
  map f (HPow.hPow (α := R[X]) X p.natDegree) +
      map f
        (∑ k ∈ Finset.range p.natDegree,
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)) =
    p
simp_rw₂ :
  map f (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ i ∈ Finset.range p.natDegree,
        map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g i) : R[X]) (HPow.hPow (α := R[X]) X i)) =
    p
simp_rw₃ :
  map f (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ Finset.range p.natDegree, map f ((C : (a : R) → R[X]) (g x)) * map f (HPow.hPow (α := R[X]) X x) =
    p
simp_rw₄ : map f X ^ p.natDegree + ∑ x ∈ Finset.range p.natDegree, map f ((C : (a : R) → R[X]) (g x)) * map f X ^ x = p
simp_rw₅ :
  HPow.hPow (α := S[X]) X p.natDegree +
      ∑ x ∈ Finset.range p.natDegree, map f ((C : (a : R) → R[X]) (g x)) * HPow.hPow (α := S[X]) X x =
    p
simp_rw₆ :
  HPow.hPow (α := S[X]) X p.natDegree +
      ∑ x ∈ Finset.range p.natDegree,
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) (g x)) : S[X]) (HPow.hPow (α := S[X]) X x) =
    p
simp_rw₇ :
  HPow.hPow (α := S[X]) X p.natDegree +
      ∑ x ∈ Finset.range p.natDegree,
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff x) : S[X]) (HPow.hPow (α := S[X]) X x) =
    p
⊢ map f q = p

Tactic:
simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]

Premises used: Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_add, Polynomial.map_X, Polynomial.map_sum, Polynomial.map_C, Polynomial.Monic.as_sum
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
⊢ map f q = p

Tactic:
have hq : map f q = p := by
    simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
hq : map f q = p
simp_rw :
  degree.{u} (R := R)
      (∑ i : Fin p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g (↑i : ℕ)) : R[X]) (HPow.hPow (α := R[X]) X (↑i : ℕ))) <
    (↑p.natDegree : WithBot ℕ)
⊢ degree.{u} (R := R)
      (∑ k ∈ Finset.range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)) <
    (↑p.natDegree : WithBot ℕ)

Tactic:
simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt]

Premises used: Fin.sum_univ_eq_sum_range, Polynomial.degree_sum_fin_lt
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
hq : map f q = p
⊢ q.Monic

Tactic:
have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
hq : map f q = p
h : q.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm, Polynomial.Monic.degree_map
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
inst_2 : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
hp : p.Monic
g : ℕ → R := fun (k : ℕ) ↦ Exists.choose (p := fun (y : R) ↦ (f : (a : R) → S) y = p.coeff k) ⋯
hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
q : R[X] :=
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ k ∈ Finset.range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (g k) : R[X]) (HPow.hPow (α := R[X]) X k)
hq : map f q = p
h : q.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
inl : ∀ (hR : Subsingleton S), ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
inr : ∀ (hR : Nontrivial S), ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
rcases subsingleton_or_nontrivial S with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ p = 1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
inl :
  ∀ (hlifts : 1 ∈ lifts f) (hp : Monic.{v} (R := S) 1),
    ∃ (q : R[X]), map f q = 1 ∧ q.natDegree = natDegree.{v} (R := S) 1 ∧ q.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
obtain rfl : p = 1 := Subsingleton.elim _ _

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic.{v} (R := S) 1
⊢ natDegree.{u} (R := R) 1 = natDegree.{v} (R := S) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic.{v} (R := S) 1
⊢ Monic.{u} (R := R) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic.{v} (R := S) 1
⊢ ∃ (q : R[X]), map f q = 1 ∧ q.natDegree = natDegree.{v} (R := S) 1 ∧ q.Monic

Tactic:
exact ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
inr :
  ∀ (p' : R[X]) (h₁ : map f p' = p) (h₂ : p'.degree = p.degree) (h₃ : p'.Monic),
    ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp

Premises used: Polynomial.lifts_and_degree_eq_and_monic
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

Premises used: And.intro, Exists.intro, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Ring R
S : Type v
inst_1 : Ring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ liftsRing f

Tactic:
simp only [lifts, liftsRing, RingHom.mem_range, RingHom.mem_rangeS]

Premises used: RingHom.mem_range, RingHom.mem_rangeS, Polynomial.lifts, Polynomial.liftsRing
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
p : S[X]
⊢ Membership.mem (γ := Subsemiring S[X]) (lifts (algebraMap R S)) p ↔
    Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) p

Tactic:
simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]

Premises used: AlgHom.mem_range, Polynomial.mapAlg_eq_map, RingHom.mem_rangeS, Polynomial.coe_mapRingHom, Polynomial.lifts
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
p : S[X]
r : R
hp : Membership.mem (γ := Subsemiring S[X]) (lifts (algebraMap R S)) p
⊢ Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) p

Tactic:
rw [mem_lifts_iff_mem_alg] at hp ⊢

Premises used: Polynomial.mem_lifts_iff_mem_alg
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
p : S[X]
r : R
hp : Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) p
⊢ Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) (r • p)

Tactic:
Subalgebra.smul_mem (mapAlg R S).range hp r

Premises used: Polynomial.mapAlg, Subalgebra.smul_mem, AlgHom.range
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
p : S[X]
r : R
hp : Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) p
⊢ Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) (r • p)

Tactic:
exact Subalgebra.smul_mem (mapAlg R S).range hp r

Premises used: Polynomial.mapAlg, Subalgebra.smul_mem, AlgHom.range
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
p : R[X]
hp : Monic.{v} (R := S) (((mapAlg R S : AlgHom.{u, u, v} R R[X] S[X]) : (a : R[X]) → S[X]) p)
⊢ p.Monic

Tactic:
monic_of_injective (FaithfulSMul.algebraMap_injective R S) hp

Premises used: FaithfulSMul.algebraMap_injective, Polynomial.monic_of_injective
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0

Tactic:
simp [mirror]

Premises used: Polynomial.mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
pos :
  ∀ (ha : a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
neg :
  ∀ (ha : ¬a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)

Tactic:
by_cases ha : a = 0