awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic
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, hp
-- 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
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) ⋯
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic
have hg : ∀ (k : ℕ), (f : (a : R) → S) (g k) = p.coeff k
Tactic: have hg k : f (g k) = p.coeff 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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
⊢ map f q = p
have 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
Tactic: simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
-- 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
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)
⊢ ∃ (q : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic
have hq : 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]
-- 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
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
⊢ 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 ℕ)
have 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 ℕ)
Tactic: simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt]
-- 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
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 : R[X]), map f q = p ∧ q.degree = p.degree ∧ q.Monic
have h : q.Monic
Tactic: have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
-- 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
hp : p.Monic
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
have inl : ∀ (hR : Subsingleton S), ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
Tactic: rcases subsingleton_or_nontrivial S with hR | hR
-- 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
hp : p.Monic
inl : ∀ (hR : Subsingleton 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
have inr : ∀ (hR : Nontrivial S), ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
Tactic: rcases subsingleton_or_nontrivial S with hR | hR
-- 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
hp : p.Monic
hR : Subsingleton S
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
have 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
Tactic: obtain rfl : p = 1 := Subsingleton.elim _ _
Cleared hypotheses: p, hlifts, 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]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ (q : R[X]), map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
have 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
Tactic: obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Lifts (hypothesis)
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 (γ := Subsemiring S[X]) (lifts (algebraMap R S)) (r • p)
have hp₁ : Membership.mem (γ := Subalgebra R S[X]) (AlgHom.range (mapAlg R S)) p
Tactic: rw [mem_lifts_iff_mem_alg] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have 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)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have 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)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have pos : Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) 0)) ((monomial n : (a : R) → R[X]) 0)
Tactic: rw [ha, monomial_zero_right, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : a = 0
pos : Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) 0)) ((monomial n : (a : R) → R[X]) 0)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have pos₁ : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
Tactic: rw [ha, monomial_zero_right, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : a = 0
pos : Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) 0)) ((monomial n : (a : R) → R[X]) 0)
pos₁ : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have pos₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [ha, monomial_zero_right, mirror_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
have neg : reverse ((monomial n : (a : R) → R[X]) a) *
    HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
  (monomial n : (a : R) → R[X]) a
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((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)
have neg₁ : reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
    HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
  (monomial n : (a : R) → R[X]) a
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((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)
have neg₂ : reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
    HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
  (monomial n : (a : R) → R[X]) a
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((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)
have neg₃ : reflect n ((monomial n : (a : R) → R[X]) a) *
    HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
  (monomial n : (a : R) → R[X]) a
Tactic: rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]