awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f).smeval x = r • f.smeval x
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f).smeval x = r • f.smeval x
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∀ (n : ℕ), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
have 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)
Tactic: rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
have 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)
Tactic: rw [lifts_iff_coeff_lifts]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ (∀ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ (↑p.coeffs : Set S) ⊆ Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)
have mp : ∀ ⦃a : S⦄, a ∈ (↑p.coeffs : Set S) → Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a
Tactic: _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a
have mp : ∀ (n : ℕ) (hn : a = p.coeff n), Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) a
Tactic: obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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 : ℕ
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
have pos : ∀ (hn : p.coeff n = 0), 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ Membership.mem (γ := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) (p.coeff n)
have neg : ∀ (hn : ¬p.coeff n = 0), 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ Membership.mem (α := S[X]) (lifts f) ((C : (a : S) → S[X]) s : S[X])
have 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])
Tactic: obtain ⟨r, rfl⟩ := Set.mem_range.1 h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ Membership.mem (α := S[X]) (lifts f) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
have 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])
Tactic: use C r
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X]) p ∈ lifts f
have hp₁ : ∃ (x : R[X]), (mapRingHom f : (a : R[X]) → S[X]) x = p
Tactic: simp only [lifts, RingHom.mem_rangeS] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ ∃ (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
have 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])
Tactic: obtain ⟨p₁, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
Goal:
R : Type u
inst : Semiring R
S : Type v
inst_1 : Semiring S
f : R →+* S
r : R
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])
have 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])
Tactic: use C r * p₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) s : S[X])
have 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])
Tactic: obtain ⟨r, rfl⟩ := Set.mem_range.1 h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ Membership.mem (α := S[X]) (lifts f) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
have 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])
Tactic: use monomial n r
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ erase n p ∈ lifts f
have rw : ∀ (h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS) (n_1 : ℕ), (erase n p).coeff n_1 ∈ f.rangeS
Tactic: rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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 : ℕ
⊢ (erase n p).coeff k ∈ f.rangeS
have pos : ∀ (hk : k = n), (erase n p).coeff k ∈ f.rangeS
Tactic: by_cases hk : k = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ (erase n p).coeff k ∈ f.rangeS
have neg : ∀ (hk : ¬k = n), (erase n p).coeff k ∈ f.rangeS
Tactic: by_cases hk : k = n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ (erase n p).coeff k ∈ f.rangeS
have h₁ : (f : (a : R) → S) 0 = (erase n p).coeff k
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ (erase n p).coeff k ∈ f.rangeS
have neg : ∀ (i : R) (hi : (f : (a : R) → S) i = p.coeff k), (erase n p).coeff k ∈ f.rangeS
Tactic: obtain ⟨i, hi⟩ := h k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ (erase n p).coeff k ∈ f.rangeS
have h₁ : (f : (a : R) → S) i = (erase n p).coeff k
Tactic: use i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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])
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_ne s 0 with rfl | h
Cleared hypotheses: s, hl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_ne s 0 with rfl | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ ∃ (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)
have 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))
Tactic: obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n
Cleared hypotheses: s, hl, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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))
have 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))
Tactic: refine ⟨monomial n a, map_monomial f, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ 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))
have inr : a ≠ 0
Tactic: rw [degree_monomial, degree_monomial n h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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]), map f q = p ∧ q.support = p.support
have hlifts₁ : ∀ (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
Cleared hypotheses: hlifts
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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) ⋯
⊢ ∃ (q : R[X]), map f q = p ∧ q.support = p.support
have hg : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ map f q = p
have simp_rw₁ : ∑ i ∈ p.support, map f ((monomial i : (a : R) → R[X]) (g i)) = p
Tactic: simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ map f q = p
have simp_rw₂ : ∑ x ∈ p.support, (monomial x : (a : S) → S[X]) ((f : (a : R) → S) (g x)) = p
Tactic: simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ map f q = p
have simp_rw₃ : ∑ x ∈ p.support, (monomial x : (a : S) → S[X]) (p.coeff x) = p
Tactic: simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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)
⊢ ∃ (q : R[X]), map f q = p ∧ q.support = p.support
have hq : map f q = p
Tactic: have hq : map f q = p := by simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
have simp_rw : ∀ (a : ℕ), g a = 0 → p.coeff a = 0
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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
⊢ p.coeff k = 0
have rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g k) : S) (0 : S)
Tactic: rw [← hg, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ p.coeff k = 0
have rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [← hg, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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)
⊢ p.coeff k = 0
have rw₂ : Eq.{v + 1} (α := S) 0 0
Tactic: rw [← hg, h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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 : R[X]), map f q = p ∧ q.support = p.support
have hq' : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (goal)
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]), map f q = p ∧ q.degree = p.degree
have 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
Tactic: obtain ⟨q, hq, hq'⟩ := exists_support_eq_of_mem_lifts hlifts