awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
add₁ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p + q).smeval x
add₂ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p.smeval x + q.smeval x)
add₃ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • p.smeval x + r • q.smeval x
add₄ :
  r • p.smeval x + (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • p.smeval x + r • q.smeval x
add₅ add₆ : r • p.smeval x + r • q.smeval x = r • p.smeval x + r • q.smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x

Tactic:
rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]

Premises used: mul_add, LaurentPolynomial.smeval_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
C_mul_T :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
          T n).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₁ :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (r * s) : R[T;T⁻¹]) (T n)).smeval x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₂ :
  (r * s) • (↑(x ^ n) : S) =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₃ : (r * s) • (↑(x ^ n) : S) = r • s • (↑(x ^ n) : S)
C_mul_T₄ C_mul_T₅ : r • s • (↑(x ^ n) : S) = r • s • (↑(x ^ n) : S)
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x

Tactic:
rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]

Premises used: mul_assoc, map_mul, LaurentPolynomial.smeval_C_mul_T_n, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
add :
  ∀ (p q : R[T;T⁻¹])
    (hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x)
    (hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x),
    (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
C_mul_T :
  ∀ (n : ℤ) (s : R),
    (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
        x =
      r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f).smeval x = r • f.smeval x

Tactic:
induction f using LaurentPolynomial.induction_on' with
  | add p q hp hq =>
    rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]

Premises used: mul_assoc, map_mul, mul_add, LaurentPolynomial.smeval_C_mul_T_n, LaurentPolynomial.smeval_add, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f_1 g : R[T;T⁻¹]
x y : Sˣ
r : R
f : R[T;T⁻¹]
⊢ (r • f).smeval x = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (f.smeval x)

Tactic:
simp [smul_eq_C_mul]

Premises used: LaurentPolynomial.smul_eq_C_mul
-- 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]
⊢ p ∈ lifts f ↔ ∃ (q : R[X]), map f q = p

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

Premises used: RingHom.mem_rangeS, Polynomial.coe_mapRingHom, Polynomial.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]
⊢ p ∈ lifts f ↔ p ∈ Set.range (map f)

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

Premises used: Set.mem_range, RingHom.mem_rangeS, Polynomial.coe_mapRingHom, Polynomial.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]
⊢ p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS

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

Premises used: RingHom.mem_rangeS, Polynomial.coe_mapRingHom, Polynomial.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]
rw :
  (∀ (n : ℕ), p.coeff n ∈ f.rangeS) ↔
    ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
⊢ 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_ringHom_rangeS, mem_map_rangeS f]

Premises used: Polynomial.lifts_iff_ringHom_rangeS, Polynomial.mem_map_rangeS
-- 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]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) ↔
    ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
rfl
-- 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]
rw :
  (∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)) ↔
    (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
⊢ p ∈ lifts f ↔ (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
rw [lifts_iff_coeff_lifts]

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]
mp :
  (∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)) →
    (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
mpr :
  (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) →
    ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
⊢ (∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)) ↔
    (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
constructor
-- 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]
h : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
mp :
  ∀ ⦃a : S⦄, a ∈ (↑p.coeffs : Set S) → Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a
⊢ (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)

Tactic:
_
-- 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]
h : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
a : S
hc : a ∈ (↑p.coeffs : Set S)
mp : ∀ (n : ℕ) (hn : a = p.coeff n), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a

Tactic:
obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc

Premises used: Iff.mp, Polynomial.mem_coeffs_iff
-- 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]
h : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
a : S
hc : a ∈ (↑p.coeffs : Set S)
n : ℕ
hn : a = p.coeff n
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a

Tactic:
hn ▸ h n

Premises used: Eq.rec, Eq.symm
-- 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]
h : ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
a : S
hc : a ∈ (↑p.coeffs : Set S)
n : ℕ
hn : a = p.coeff n
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a

Tactic:
exact hn ▸ h n
-- 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]
h : (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
n : ℕ
pos : ∀ (hn : p.coeff n = 0), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
neg :
  ∀ (hn : ¬p.coeff n = 0), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
by_cases hn : p.coeff n = 0

Premises used: Polynomial.coeff
-- 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]
h : (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
n : ℕ
hn : p.coeff n = 0
⊢ (f : (a : R) → S) 0 = p.coeff n

Tactic:
simp [hn]
-- 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]
h : (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
n : ℕ
hn : p.coeff n = 0
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
exact ⟨0, by simp [hn]⟩
-- 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]
h : (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
n : ℕ
hn : ¬p.coeff n = 0
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
h <| coeff_mem_coeffs hn

Premises used: Polynomial.coeff_mem_coeffs
-- 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]
h : (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
n : ℕ
hn : ¬p.coeff n = 0
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)

Tactic:
exact h <| coeff_mem_coeffs hn

Premises used: Polynomial.coeff_mem_coeffs
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : S[X]
⊢ p ∈ lifts f

Tactic:
(lifts_iff_coeff_lifts p).mpr fun n ↦ hf (p.coeff n)

Premises used: Iff.mpr, Polynomial.coeff, 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
r : R
⊢ Eq (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) ((C : (a : R) → R[X]) r) : S[X])
    ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])

Tactic:
simp only [coe_mapRingHom, map_C]

Premises used: Polynomial.coe_mapRingHom, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
s : S
h : Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) s
obtain :
  ∀ (r : R)
    (h :
      Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
        ((f : (a : R) → S) r : S)),
    Membership.mem (α := S[X]) (lifts f) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
⊢ Membership.mem (α := S[X]) (lifts f) ((C : (a : S) → S[X]) s : S[X])

Tactic:
obtain ⟨r, rfl⟩ := Set.mem_range.1 h

Premises used: Set.mem_range, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
r : R
h :
  Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
    ((f : (a : R) → S) r : S)
h₁ :
  Eq (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) ((C : (a : R) → R[X]) r) : S[X])
    ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
⊢ Membership.mem (α := S[X]) (lifts f) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])

Tactic:
use C r

Premises used: Polynomial.C, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
r : R
h :
  Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
    ((f : (a : R) → S) r : S)
⊢ Eq (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) ((C : (a : R) → R[X]) r) : S[X])
    ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])

Tactic:
simp only [coe_mapRingHom, map_C]

Premises used: Polynomial.coe_mapRingHom, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
⊢ Eq.{v + 1} (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) X : S[X]) (X : S[X])

Tactic:
simp only [coe_mapRingHom, map_X]

Premises used: Polynomial.map_X, Polynomial.coe_mapRingHom
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ (mapRingHom f : (a : R[X]) → S[X]) (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := S[X]) X n

Tactic:
simp only [coe_mapRingHom, map_pow, map_X]

Premises used: Polynomial.map_X, map_pow, Polynomial.coe_mapRingHom
-- 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]
r : R
hp : p ∈ lifts f
⊢ ∃ (x : R[X]), (mapRingHom f : (a : R[X]) → S[X]) x = p

Tactic:
simp only [lifts, RingHom.mem_rangeS] at hp ⊢

Premises used: RingHom.mem_rangeS, Polynomial.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]
r : R
hp : ∃ (x : R[X]), (mapRingHom f : (a : R[X]) → S[X]) x = p
obtain :
  ∀ (p₁ : R[X]),
    ∃ (x : R[X]),
      (mapRingHom f : (a : R[X]) → S[X]) x =
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
          ((mapRingHom f : (a : R[X]) → S[X]) p₁ : S[X])
⊢ ∃ (x : R[X]),
    (mapRingHom f : (a : R[X]) → S[X]) x = HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X]) p

Tactic:
obtain ⟨p₁, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
r : R
p₁ : R[X]
h :
  (mapRingHom f : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p₁) =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
      ((mapRingHom f : (a : R[X]) → S[X]) p₁ : S[X])
⊢ ∃ (x : R[X]),
    (mapRingHom f : (a : R[X]) → S[X]) x =
      HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
        ((mapRingHom f : (a : R[X]) → S[X]) p₁ : S[X])

Tactic:
use C r * p₁

Premises used: Polynomial.C, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ (mapRingHom f : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p₁) =
    HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
      ((mapRingHom f : (a : R[X]) → S[X]) p₁ : S[X])

Tactic:
simp only [coe_mapRingHom, map_C, map_mul]

Premises used: map_mul, Polynomial.coe_mapRingHom, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
s : S
n : ℕ
h : Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) s
obtain :
  ∀ (r : R)
    (h :
      Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
        ((f : (a : R) → S) r : S)),
    Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
⊢ Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) s : S[X])

Tactic:
obtain ⟨r, rfl⟩ := Set.mem_range.1 h

Premises used: Set.mem_range, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
r : R
h :
  Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
    ((f : (a : R) → S) r : S)
h₁ :
  Eq (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) r) : S[X])
    ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
⊢ Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])

Tactic:
use monomial n r

Premises used: Polynomial.monomial, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
r : R
h :
  Membership.mem.{v, v} (α := S) (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S))
    ((f : (a : R) → S) r : S)
⊢ Eq (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) r) : S[X])
    ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])

Tactic:
simp only [coe_mapRingHom, map_monomial]

Premises used: Polynomial.map_monomial, Polynomial.coe_mapRingHom
-- 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]
n : ℕ
h : p ∈ lifts f
rw : ∀ (h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS) (n_1 : ℕ), (erase n p).coeff n_1 ∈ f.rangeS
⊢ erase n p ∈ lifts f

Tactic:
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h ⊢

Premises used: Polynomial.lifts_iff_ringHom_rangeS, Polynomial.mem_map_rangeS
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
pos : ∀ (hk : k = n), (erase n p).coeff k ∈ f.rangeS
neg : ∀ (hk : ¬k = n), (erase n p).coeff k ∈ f.rangeS
⊢ (erase n p).coeff k ∈ f.rangeS

Tactic:
by_cases hk : k = n
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : k = n
h₁ : (f : (a : R) → S) 0 = (erase n p).coeff k
⊢ (erase n p).coeff k ∈ f.rangeS

Tactic:
use 0
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : k = n
⊢ (f : (a : R) → S) 0 = (erase n p).coeff k

Tactic:
simp only [hk, map_zero, erase_same]

Premises used: map_zero, Polynomial.erase_same
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
neg : ∀ (i : R) (hi : (f : (a : R) → S) i = p.coeff k), (erase n p).coeff k ∈ f.rangeS
⊢ (erase n p).coeff k ∈ f.rangeS

Tactic:
obtain ⟨i, hi⟩ := h k
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
i : R
hi : (f : (a : R) → S) i = p.coeff k
h₁ : (f : (a : R) → S) i = (erase n p).coeff k
⊢ (erase n p).coeff k ∈ f.rangeS

Tactic:
use i
-- 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]
n : ℕ
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
k : ℕ
hk : ¬k = n
i : R
hi : (f : (a : R) → S) i = p.coeff k
⊢ (f : (a : R) → S) i = (erase n p).coeff k

Tactic:
simp only [hi, hk, erase_ne, Ne, not_false_iff]

Premises used: Ne, Polynomial.erase_ne, not_false_iff
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
s : S
n : ℕ
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) s : S[X])
inl :
  ∀ (hl : (monomial n : (a : S) → S[X]) 0 ∈ lifts f),
    ∃ (q : R[X]),
      map f q = (monomial n : (a : S) → S[X]) 0 ∧ q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) 0)
inr :
  ∀ (h : s ≠ 0),
    ∃ (q : R[X]),
      map f q = (monomial n : (a : S) → S[X]) s ∧ q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) s)
⊢ ∃ (q : R[X]),
    map f q = (monomial n : (a : S) → S[X]) s ∧ q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) s)

Tactic:
rcases eq_or_ne s 0 with rfl | h

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n : (a : S) → S[X]) 0 ∈ lifts f
⊢ map f 0 = (monomial n : (a : S) → S[X]) 0 ∧
    degree.{u} (R := R) 0 = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n : (a : S) → S[X]) 0 ∈ lifts f
⊢ ∃ (q : R[X]),
    map f q = (monomial n : (a : S) → S[X]) 0 ∧ q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) 0)

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.Polynomial.Lifts
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
s : S
n : ℕ
hl : Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) s : S[X])
h : s ≠ 0
inr :
  ∀ (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)),
    ∃ (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))
⊢ ∃ (q : R[X]),
    map f q = (monomial n : (a : S) → S[X]) s ∧ q.degree = degree.{v} (R := S) ((monomial n : (a : S) → S[X]) s)

Tactic:
obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n

Premises used: rfl
-- 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)
⊢ ∃ (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:
⟨monomial n a, map_monomial f, ?_⟩

Premises used: Polynomial.map_monomial, Polynomial.monomial, And.intro, Exists.intro, DFunLike.coe