mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₂.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

pp: case h₂.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m

Tactic:
<;>

Goal state after:
case h₂.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

case h₂.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ (sSupFun hc).domain
⊢ 0 < ↑(sSupFun hc) (y - x)

Tactic:
simp_rw [sSupFun, LinearPMap.domain_sSup] at hyx

Goal state after:
K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
⊢ 0 < ↑(sSupFun hc) (y - x)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial.add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
n : ℕ
p✝ q✝ : R[X]
a✝¹ : eval x ((aeval (C y)) ((aeval Y) p✝)) * x ^ n = (aeval y) p✝ * x ^ n
a✝ : eval x ((aeval (C y)) ((aeval Y) q✝)) * x ^ n = (aeval y) q✝ * x ^ n
⊢ eval x ((aeval (C y)) ((aeval Y) (p✝ + q✝))) * x ^ n = (aeval y) (p✝ + q✝) * x ^ n

pp: case monomial.monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
n n✝ : ℕ
a✝ : R
⊢ eval x ((aeval (C y)) ((aeval Y) ((monomial n✝) a✝))) * x ^ n = (aeval y) ((monomial n✝) a✝) * x ^ n

Tactic:
<;>

Goal state after:
case monomial.add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
n : ℕ
p✝ q✝ : R[X]
a✝¹ : eval x ((aeval (C y)) ((aeval Y) p✝)) * x ^ n = (aeval y) p✝ * x ^ n
a✝ : eval x ((aeval (C y)) ((aeval Y) q✝)) * x ^ n = (aeval y) q✝ * x ^ n
⊢ eval x ((aeval (C y)) ((aeval Y) (p✝ + q✝))) * x ^ n = (aeval y) (p✝ + q✝) * x ^ n

case monomial.monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
n n✝ : ℕ
a✝ : R
⊢ eval x ((aeval (C y)) ((aeval Y) ((monomial n✝) a✝))) * x ^ n = (aeval y) ((monomial n✝) a✝) * x ^ n
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial.add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
n : ℕ
p✝ q✝ : R[X]
a✝¹ : map (algebraMap R A) p✝ * C x ^ n = map (↑(aeval x)) ((aeval Y) p✝) * C x ^ n
a✝ : map (algebraMap R A) q✝ * C x ^ n = map (↑(aeval x)) ((aeval Y) q✝) * C x ^ n
⊢ map (algebraMap R A) (p✝ + q✝) * C x ^ n = map (↑(aeval x)) ((aeval Y) (p✝ + q✝)) * C x ^ n

pp: case monomial.monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
n n✝ : ℕ
a✝ : R
⊢ map (algebraMap R A) ((monomial n✝) a✝) * C x ^ n = map (↑(aeval x)) ((aeval Y) ((monomial n✝) a✝)) * C x ^ n

Tactic:
<;>

Goal state after:
case monomial.add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
n : ℕ
p✝ q✝ : R[X]
a✝¹ : map (algebraMap R A) p✝ * C x ^ n = map (↑(aeval x)) ((aeval Y) p✝) * C x ^ n
a✝ : map (algebraMap R A) q✝ * C x ^ n = map (↑(aeval x)) ((aeval Y) q✝) * C x ^ n
⊢ map (algebraMap R A) (p✝ + q✝) * C x ^ n = map (↑(aeval x)) ((aeval Y) (p✝ + q✝)) * C x ^ n

case monomial.monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
n n✝ : ℕ
a✝ : R
⊢ map (algebraMap R A) ((monomial n✝) a✝) * C x ^ n = map (↑(aeval x)) ((aeval Y) ((monomial n✝) a✝)) * C x ^ n
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case pos.refine_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ q.coeff (i - (deg(p) - deg(q))) ∈ span R coeffs(q)

pp: case pos.refine_2
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ p.leadingCoeff ∈ span R coeffs(p)

Tactic:
<;>

Goal state after:
case pos.refine_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ q.coeff (i - (deg(p) - deg(q))) ∈ span R coeffs(q)

case pos.refine_2
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
h✝ : deg(p) - deg(q) ≤ i
⊢ p.leadingCoeff ∈ span R coeffs(p)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
m✝ : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)).comp (MvPolynomial.aeval ![C X, Y]))
        (MvPolynomial.X ((fun i ↦ i) ⟨0, ⋯⟩))) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial (Fin 2) R)) (MvPolynomial.X ((fun i ↦ i) ⟨0, ⋯⟩)))

pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
m✝ : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)).comp (MvPolynomial.aeval ![C X, Y]))
        (MvPolynomial.X ((fun i ↦ i) ⟨1, ⋯⟩))) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial (Fin 2) R)) (MvPolynomial.X ((fun i ↦ i) ⟨1, ⋯⟩)))

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommSemiring R
m✝ : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)).comp (MvPolynomial.aeval ![C X, Y]))
        (MvPolynomial.X ((fun i ↦ i) ⟨0, ⋯⟩))) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial (Fin 2) R)) (MvPolynomial.X ((fun i ↦ i) ⟨0, ⋯⟩)))

case «1»
R : Type u_1
inst✝ : CommSemiring R
m✝ : Fin 2 →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)).comp (MvPolynomial.aeval ![C X, Y]))
        (MvPolynomial.X ((fun i ↦ i) ⟨1, ⋯⟩))) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial (Fin 2) R)) (MvPolynomial.X ((fun i ↦ i) ⟨1, ⋯⟩)))
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case hC
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ (((((MvPolynomial.aeval ![C X, Y]).comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))).comp CAlgHom) X).coeff
          n✝¹).coeff
      n✝ =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n✝¹).coeff n✝

pp: case hX
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ ((((MvPolynomial.aeval ![C X, Y]).comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))) Y).coeff n✝¹).coeff n✝ =
    (((AlgHom.id R R[X][Y]) Y).coeff n✝¹).coeff n✝

Tactic:
<;>

Goal state after:
case hC
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ (((((MvPolynomial.aeval ![C X, Y]).comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))).comp CAlgHom) X).coeff
          n✝¹).coeff
      n✝ =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n✝¹).coeff n✝

case hX
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ ((((MvPolynomial.aeval ![C X, Y]).comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))) Y).coeff n✝¹).coeff n✝ =
    (((AlgHom.id R R[X][Y]) Y).coeff n✝¹).coeff n✝
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ ∃ a b, f = X ^ 2 + C (-a) * X + C b

Tactic:
obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
a b : R
h : f = X ^ 2 + C a * X + C b
⊢ ∃ a b, f = X ^ 2 + C (-a) * X + C b
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ a) → IsUnit a

pp: case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ b) → IsUnit b

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ a) → IsUnit a

case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit (map φ b) → IsUnit b
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a.leadingCoeff

pp: case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b.leadingCoeff

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit a.leadingCoeff

case refine_2
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b.leadingCoeff
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : i = deg(p) - deg(q)
⊢ p.leadingCoeff * 1 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : ¬i = deg(p) - deg(q)
⊢ p.leadingCoeff * 0 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
<;>

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : i = deg(p) - deg(q)
⊢ p.leadingCoeff * 1 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
h✝ : ¬i = deg(p) - deg(q)
⊢ p.leadingCoeff * 0 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: case e_a.e_a.e_x.e_a.refine_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bg = 1

pp: case e_a.e_a.e_x.e_a.refine_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bf = 1

Tactic:
<;>

Goal state after:
case e_a.e_a.e_x.e_a.refine_1
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bg = 1

case e_a.e_a.e_x.e_a.refine_2
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
a b : R
N : ℕ
f g : R[X]
x✝¹ : DenomsClearable a b N f i
x✝ : DenomsClearable a b N g i
Df : R
bf : K
bfu : bf * i b = 1
Hf : i Df = i b ^ N * eval (i a * bf) (Polynomial.map i f)
Dg : R
bg : K
bgu : bg * i b = 1
Hg : i Dg = i b ^ N * eval (i a * bg) (Polynomial.map i g)
⊢ i b * bf = 1
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg.refine_3
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
· exact H'' (coeff_divModByMonicAux_mem_span_pow_mul_span _ _ hq i).2

Goal state after:
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case hab
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ≤ Mq

pp: case h₂
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(p) ≤ Mp

Tactic:
<;>

Goal state after:
case hab
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ≤ Mq

case h₂
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(p) ≤ Mp
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
this : p.coeff i = 0
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]

pp: case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case hn
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ p.natDegree ≤ n

pp: case hg
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ g 1 = 1

Tactic:
<;>

Goal state after:
case hn
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ p.natDegree ≤ n

case hg
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ g 1 = 1
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (aeval (![X, 1] 0)) p = p

pp: case hn
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p.natDegree ≤ n

pp: case hg
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ![X, 1] 1 = 1

Tactic:
<;>

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (aeval (![X, 1] 0)) p = p

case hn
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p.natDegree ≤ n

case hg
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ![X, 1] 1 = 1
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

pp: case neg
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : ¬R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)

case neg
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
hr : ¬R a b
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R a b then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
hab : R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
hab : ¬R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
hab : R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
hab : ¬R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length