mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
        (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
            (c₁ * c₂) *
          m.sPolynomial p₁ p₂
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

Tactic:
·

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
        (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
            (c₁ * c₂) *
          m.sPolynomial p₁ p₂
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.1 = (b1 * b2).gcd (a1 * b1)

pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.1 = (b1 * b2).gcd (a1 * b1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop → s.Infinite

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop → s.Infinite
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ q₁ q₂ : MvPolynomial σ R),
    p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0 →
      m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
        (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
          m.sPolynomial q₁ q₂
H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

Tactic:
·

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ q₁ q₂ : MvPolynomial σ R),
    p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0 →
      m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
        (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
          m.sPolynomial q₁ q₂
H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.snd.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.2

Tactic:
·

Goal state after:
case i_inj.snd.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.2
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : q ∈ {t | ↑t < a + b}
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ b_1 ∈ insert b B, m.toSyn (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : m.toSyn (m.degree (∑ b ∈ insert b B, g b)) < d
hb0 : g b = 0
⊢ ∃ c, ∑ b ∈ insert b B, g b = ∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ b_1 ∈ insert b B, m.toSyn (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : m.toSyn (m.degree (∑ b ∈ insert b B, g b)) < d
hb0 : ¬g b = 0
⊢ ∃ c, ∑ b ∈ insert b B, g b = ∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
d : m.syn
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
h :
  (∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < d →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ b_1 ∈ insert b B, m.toSyn (m.degree (g b_1)) = d ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0
hfd : m.toSyn (m.degree (∑ b ∈ insert b B, g b)) < d
hb0 : g b = 0
⊢ ∃ c, ∑ b ∈ insert b B, g b = ∑ b₁ ∈ insert b B, ∑ b₂ ∈ insert b B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = (b1 * b2).gcd (a2 * b2)

pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = (b1 * b2).gcd (a2 * b2)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : ↑q < a
⊢ ↑q < inducedMap α β a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap α β a ↔ ↑q < a

Tactic:
by
  refine ⟨fun h => ?_, fun hq => ?_⟩
  · rw [← inducedMap_rat α] at h
    exact (inducedMap_mono α β).reflect_lt h
  · obtain ⟨q', hq, hqa⟩ := exists_rat_btwn hq
    apply lt_csSup_of_lt (cutMap_bddAbove β a) (coe_mem_cutMap_iff.mpr hqa)
    exact mod_cast hq

Goal state after: