mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
⊢ X i ∣ p → X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
· intro hip
      refine ⟨hip, ?_⟩
      rw [X_dvd_iff_modMonomial_eq_zero] at hip
      rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp
      use r

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p = X i * p.divMonomial (Finsupp.single i 1)

Tactic:
conv_lhs => rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]

Goal state after:
case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p.modMonomial (Finsupp.single i 1) + (monomial (Finsupp.single i 1)) 1 * p.divMonomial (Finsupp.single i 1) =
    X i * p.divMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
⊢ coeff 0 ((expand p) φ) = coeff (p • 0) ((expand p) φ)

Tactic:
smul_zero

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
⊢ coeff 0 ((expand p) φ) = coeff 0 ((expand p) φ)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∏ i ∈ s, 2 ^ f i) * (∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ((∏ x ∈ s, 2 ^ f x) * ∏ x ∈ s, (f x)!)

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
m : Multiset ℕ
⊢ (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial

Tactic:
obtain ⟨l, rfl⟩ := Quotient.exists_rep m

Goal state after:
x : ℕ
l : List ℕ
⊢ (x ::ₘ ⟦l⟧).multinomial = (x + sum ⟦l⟧).choose x * multinomial ⟦l⟧
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k * m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + k * m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : degree (ofDegLex x) < degree (ofDegLex y)
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : ¬degree (ofDegLex x) < degree (ofDegLex y)
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
· simp [k]

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : ¬degree (ofDegLex x) < degree (ofDegLex y)
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ p ∣ r • (monomial (Finsupp.single i 1)) 1 ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)

Tactic:
smul_monomial,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ p ∣ (monomial (Finsupp.single i 1)) (r • 1) ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) → b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1)

pp: case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1) → ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

Tactic:
· rintro ⟨m, hmn, hb, rfl⟩
    simp only [hb, true_and]
    suffices m = 0 ∨ m = Finsupp.single i 1 by
      apply this.imp <;> simp +contextual [smul_monomial, smul_eq_mul, mul_one]
    by_cases hm : m i = 0
    · left
      ext j
      simp only [Finsupp.coe_zero, Pi.zero_apply, ← Nat.le_zero]
      by_cases hj : j = i
      · rw [← hm, hj]
      · exact (hmn j).trans (Finsupp.single_eq_of_ne hj).le
    · right
      ext j
      apply le_antisymm (hmn j)
      by_cases hj : j = i
      · simpa [hj, Nat.one_le_iff_ne_zero]
      · simp [Finsupp.single_eq_of_ne hj]

Goal state after:
case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1) → ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ ((monomial d) c).support.sup ⇑m.toSyn ≤ m.toSyn d

Tactic:
apply le_trans (Finset.sup_mono support_monomial_subset)

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ {d}.sup ⇑m.toSyn ≤ m.toSyn d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff f ≠ 0

Tactic:
leadingCoeff_ne_zero_iff

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
n✝ n k : ℕ
s : { s // 0 ∉ s }
⊢ (fun s ↦ ⟨map (Fin.succAbove 0) s, ⋯⟩) ((fun s ↦ map (Fin.predAbove 0) ↑s) s) = s

Tactic:
by
    ext1
    simp only [map_map]
    refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
    exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (0 ^ n) = n • 0

Tactic:
smul_zero

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (0 ^ n) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.leadingCoeff f ≠ 0

Tactic:
leadingCoeff_ne_zero_iff

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ f ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ n.MinSqFacProp (some k)

pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ n.MinSqFacProp ((n / k).minSqFacAux (k + 2))

pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux (k + 2))

Tactic:
· exact ⟨pk dk, (Nat.dvd_div_iff_mul_dvd dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩

Goal state after:
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ n.MinSqFacProp ((n / k).minSqFacAux (k + 2))

case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux (k + 2))
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ f m✝ * f n✝ * (g m✝ * g n✝) = f m✝ * g m✝ * (f n✝ * g n✝)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree g) g * coeff (m.degree f) f - coeff (m.degree f) f * coeff (m.degree g) g = 0

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
⊢ C (m.leadingCoeff g) * C (m.leadingCoeff f) - C (m.leadingCoeff f) * C (m.leadingCoeff g) = 0

Tactic:
ring

Goal state after:
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
⊢ (f * g) 1 = 1

Tactic:
simp [hf.1, hg.1]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
primeFactorsList_eq_nil

Goal state after:
n : ℕ
⊢ n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList ≠ [] ↔ 1 < n

Tactic:
primeFactorsList_ne_nil

Goal state after:
n : ℕ
⊢ 1 < n ↔ 1 < n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case hi.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : (a1 * a2).Coprime (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case neg.succ
m : ℕ
hm : ¬m = 0
n : ℕ
ih : Ω (m ^ n) = n * Ω m
⊢ n * Ω m + Ω m = (n + 1) * Ω m

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2

Tactic:
rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 1).Coprime (a 2)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
⊢ ∃ a_1,
    ∀ (b : ℕ),
      a_1 ≤ b → ∑ k ∈ Finset.range b, s.indicator (fun x ↦ a) k = ∑ a_3 ∈ hs.toFinset, s.indicator (fun x ↦ a) a_3

Tactic:
refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩ <;> intro x

Goal state after:
case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ hs.toFinset → x ∈ Finset.range n

case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ hs.toFinset → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0
hfd : 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₂)

Tactic:
refine m.sPolynomial_decomposition ?_ hfd

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0
hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d
⊢ ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case h
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
⊢ f ((a1, a2), b1, b2).1.1 * g ((a1, a2), b1, b2).1.2 * (f ((a1, a2), b1, b2).2.1 * g ((a1, a2), b1, b2).2.2) =
    f ((a1, a2), b1, b2).1.1 * f ((a1, a2), b1, b2).2.1 * (g ((a1, a2), b1, b2).1.2 * g ((a1, a2), b1, b2).2.2)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #(range #s) • ∑ i ∈ s, f i • g i

Tactic:
sum_smul_sum_eq_sum_perm hσ

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i) ≤ #(range #s) • ∑ i ∈ s, f i • g i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
α : Type u_2
f : M → α
h : ∀ (a b : M), mk a = mk b → f a = f b
a : M
⊢ lift f h (mk a) = f a

Tactic:
unfold lift
  exact Quotient.lift_mk f (fun _ _ h' ↦ h _ _ <| mk_eq_mk.mpr h') a

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
⊢ f (x.lcm y) * f (x.gcd y) = f x * f y

Tactic:
by
  by_cases hx : x = 0
  · simp only [hx, f.map_zero, zero_mul, lcm_zero_left, gcd_zero_left]
  by_cases hy : y = 0
  · simp only [hy, f.map_zero, mul_zero, lcm_zero_right, gcd_zero_right, zero_mul]
  have hgcd_ne_zero : x.gcd y ≠ 0 := gcd_ne_zero_left hx
  have hlcm_ne_zero : x.lcm y ≠ 0 := lcm_ne_zero hx hy
  have hfi_zero : ∀ {i}, f (i ^ 0) = 1 := by
    intro i; rw [pow_zero, hf.1]
  iterate 4 rw [hf.multiplicative_factorization f (by assumption),
    Finsupp.prod_of_support_subset _ _ _ (fun _ _ => hfi_zero)
      (s := (x.primeFactors ∪ y.primeFactors))]
  · rw [← prod_mul_distrib, ← prod_mul_distrib]
    apply prod_congr rfl
    intro p _
    rcases Nat.le_or_le (x.factorization p) (y.factorization p) with h | h <;>
      simp only [factorization_lcm hx hy, Finsupp.sup_apply, h, sup_of_le_right,
        sup_of_le_left, inf_of_le_right, factorization_gcd hx hy, Finsupp.inf_apply,
        inf_of_le_left, mul_comm]
  · apply subset_union_right
  · apply subset_union_left
  · rw [factorization_gcd hx hy, Finsupp.support_inf]
    apply inter_subset_union
  · simp [factorization_lcm hx hy]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk (a i * ∏ x ∈ s, a x) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
rw [mul_comm, mk_mul_eq_mk_left hlt, ih]

Goal state after:
case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk (a (s.min' hs)) = mk (a ((Finset.cons i s hi).min' ⋯))
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(inl M₀ N₀)

Tactic:
by
  refine (WithZero.map'_mono MonoidHom.inl_mono).comp ?_
  intro x y
  obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y <;>
  · simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Icc a b).val = (Finset.image (fun x ↦ c + x) (Finset.Icc a b)).val

Tactic:
Finset.image_val,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Icc a b).val = (map (fun x ↦ c + x) (Finset.Icc a b).val).dedup
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ico a b).val = (Finset.image (fun x ↦ c + x) (Finset.Ico a b)).val

Tactic:
Finset.image_val,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ico a b).val = (map (fun x ↦ c + x) (Finset.Ico a b).val).dedup
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = (Finset.image (fun x ↦ c + x) (Finset.Ioc a b)).val

Tactic:
Finset.image_val,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = (map (fun x ↦ c + x) (Finset.Ioc a b).val).dedup
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = (Finset.image (fun x ↦ c + x) (Finset.Ioo a b)).val

Tactic:
Finset.image_val,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = (map (fun x ↦ c + x) (Finset.Ioo a b).val).dedup
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : x✝ ⊆ {⊥}
⊢ s ≤ ⊥

Tactic:
exact (h ha).le

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ ∀ (a b : Interval α), a - b = a + -b

Tactic:
by
    rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

Goal state after: