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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H : (expand n) g = (expand n) g'
d : σ →₀ ℕ
⊢ coeff d g = coeff d g'

Tactic:
← coeff_expand_smul _ (n.ne_zero_iff_zero_lt.mpr hn),

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : MvPolynomial σ R
H : (expand n) g = (expand n) g'
d : σ →₀ ℕ
⊢ coeff (n • d) ((expand n) g) = coeff d g'
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ ∀ (n : ℕ), ∅.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
| empty =>

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

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) 1 * r ∣ (monomial m) 1 * (monomial (n - m)) 1 * q

Tactic:
mul_assoc

Goal state after:
case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) 1 * r ∣ (monomial m) 1 * ((monomial (n - m)) 1 * q)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
⊢ s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).countPerms * (Multiset.map x ↑k).prod

Tactic:
conv_rhs => rw [← sum_coe_sort]
  convert! sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n
  rw [Multiset.noncommProd_eq_prod]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s) = ↑s

Tactic:
coe_fill,

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) (↑s + ↑(replicate (↑m) x)) = ↑s
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty
m' : Multiset ℕ
⊢ (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial

Tactic:
| empty =>

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

Goal state before:
pp: case empty
⊢ 0 < multinomial 0

Tactic:
| empty =>

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot m.syn
⊢ m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥

Tactic:
simp [m.toWithBotSyn.symm_apply_eq]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ ∀ (x : Π₀ (i : ι), α i), x.support = ∅ → (∀ i ∈ ∅, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
| empty =>

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

Goal state before:
pp: case inr.empty
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
h : ∀ i ∈ ∅, f i ≠ 0
⊢ degreeOf n (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, degreeOf n (f i)

Tactic:
| empty =>

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ¬(Polynomial.C (C c)).leadingCoeff *
        ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff =
      0

Tactic:
Polynomial.leadingCoeff_C

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ¬C c * ((optionEquivLeft R { b // ¬b = j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
⊢ m.toSyn (m.degree (∑ x ∈ ∅, f x)) ≤ ∅.sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
| empty =>

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
rw [add_comm, degree_add_of_lt (h' h), right_eq_sup]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ False

Tactic:
revert h

Goal state after:
case zero
b : ℕ
⊢ DvdNotUnit 0 b → False
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
hf' : m.toSyn d ≤ m.toSyn (m.degree g)
⊢ m.toSyn a + m.toSyn b ≤ m.toSyn c + m.toSyn b

Tactic:
rw [← map_add, ← hcd, map_add]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn c ≤ m.toSyn (m.degree f)
hf' : m.toSyn d ≤ m.toSyn (m.degree g)
⊢ m.toSyn c + m.toSyn d ≤ m.toSyn c + m.toSyn b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree (∏ i ∈ ∅, P i)) ≤ m.toSyn (∑ i ∈ ∅, m.degree (P i))

Tactic:
simp only [Finset.prod_empty, Finset.sum_empty]

Goal state after:
case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree 1) ≤ m.toSyn 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree (∏ i ∈ ∅, P i)) ≤ m.toSyn (∑ i ∈ ∅, m.degree (P i))

Tactic:
| empty =>

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

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ coeff (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i) = ∏ i ∈ ∅, m.leadingCoeff (P i)

Tactic:
| empty =>

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)

Tactic:
by_cases h0 : f * g = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h0 : f * g = 0
⊢ m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h0 : ¬f * g = 0
⊢ m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ ∅, f x)) ≤ ∅.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
| empty =>

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ d ∈ n.divisors with Squarefree d, f d = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod

Tactic:
Finset.sum_eq_multiset_sum,

Goal state after:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map f {d ∈ n.divisors | Squarefree d}.val).sum = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
unfold degree
  rw [support_neg]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ ¬IsPrimePow n ↔ n.primeFactors.Nontrivial

Tactic:
rw [isPrimePow_iff_card_primeFactors_eq_one, ← Finset.one_lt_card_iff_nontrivial]
  grind [primeFactors_eq_empty]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1

pp: case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
· cases not_isPrimePow_zero h

Goal state after:
case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case empty
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
hs : (↑∅).Pairwise (Coprime on g)
⊢ f (∏ i ∈ ∅, g i) = ∏ i ∈ ∅, f (g i)

Tactic:
| empty =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = ∑ i ∈ n.divisors, f i * g (n / i)

Tactic:
← divisors_filter_squarefree_of_squarefree hn,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ t ∈ n.primeFactors.powerset, (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i =
    ∑ i ∈ n.divisors with Squarefree i, f i * g (n / i)
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · simp only [Nat.coprime_zero_left] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp only [Nat.coprime_zero_right] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  ext n
  simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true, Ne,
    and_congr_left_iff, not_false_iff, Nat.mem_divisors, or_self_iff]
  apply hab.isPrimePow_dvd_mul

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

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ↑(∏ x_1, x x_1) = n ∧ (fun x_1 ↦ ↑(x x_1)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
PNat.coe_prod

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i, ↑(x i) = n ∧ (fun i ↦ ↑(x i)) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case empty
h0 : Multiset.prod 0 ≠ 0
⊢ Ω (Multiset.prod 0) = (Multiset.map (⇑Ω) 0).sum

Tactic:
| empty =>

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

Goal state before:
pp: n d : ℕ
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n

Tactic:
← hf.1

Goal state after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case empty
ι : Type u_2
f : ι → ℕ
h : (↑∅).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, ω (f i)

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hxy : x ≠ y
⊢ x ∈ ↑(cons a s ha)

Tactic:
by simp [hx]

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

Goal state before:
pp: case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ x, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0

Tactic:
← Finset.mul_prod_erase (h := mem_univ i),

Goal state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ((if i = i then k else if i = i' then r else 1) * ∏ x ∈ univ.erase i, if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
| empty =>

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

Goal state before:
pp: case empty
ι : 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 α β
f : ι → α
g : ι → β
σ : Perm ι
hfg : MonovaryOn f g ↑∅
hσ : {x | σ x ≠ x} ⊆ ↑∅
⊢ ∑ i ∈ ∅, f i • g (σ i) ≤ ∑ i ∈ ∅, f i • g i

Tactic:
| empty =>

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i = ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i)

Tactic:
mul_assoc

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i) = ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ 1 < b

Tactic:
by
  suffices a⁻¹ < b / a by
    simpa using this
  apply lt_of_mk_lt_mk_of_le_one
  · simpa using hab
  · simpa using ha.le

Goal state after:
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsPWO
ht : t.IsPWO
⊢ ((fun x ↦ x.1 * x.2) '' s ×ˢ t).IsPWO

Tactic:
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
⊢ ((truncLT c) (x + y)).coeff i = ((truncLT c) x + (truncLT c) y).coeff i

Tactic:
by_cases h : i < c

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : i < c
⊢ ((truncLT c) (x + y)).coeff i = ((truncLT c) x + (truncLT c) y).coeff i

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : ¬i < c
⊢ ((truncLT c) (x + y)).coeff i = ((truncLT c) x + (truncLT c) y).coeff i
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c ≤ b + c

Tactic:
apply le_of_lt

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a b : Lex R⟦Γ⟧
hab : a ≤ b
c : Lex R⟦Γ⟧
hlt : a < b
⊢ a + c < b + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a : M
u : Mˣ
⊢ 1 ≤ a * ↑u⁻¹ ↔ ↑u ≤ a

Tactic:
u.le_mul_inv_iff,

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a : M
u : Mˣ
⊢ 1 * ↑u ≤ a ↔ ↑u ≤ a
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : R
⊢ mk (x * y * z) = mk (x * (y * z))

Tactic:
mul_assoc

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : ArchimedeanClass R
⊢ ⊤ + x = ⊤

Tactic:
by induction x with | mk x => rw [← mk_zero, ← mk_mul, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case empty
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
hs : 0 ≠ 0
⊢ ∃ b ∈ 0, f (Multiset.map g 0).sum ≤ f (g b)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case empty
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
⊢ ∃ b, (0 ≠ 0 → b ∈ 0) ∧ f (Multiset.map g 0).sum ≤ f (g b)

Tactic:
| empty =>

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
⊢ ∃ n, ↑n < x

Tactic:
by
  obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg (mk_neg x ▸ hx)
  use -n
  simpa [neg_lt]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R✝¹ : Type u_1
inst✝² : CommRing R✝¹
P✝¹ : RingPreordering R✝¹
R✝ : Type u_2
inst✝¹ : CommRing R✝
P✝ : Set R✝
add✝ : ?m.2
mul✝ : ?m.3
sq✝ : ?m.4
neg_one✝ : ?m.5
R : Type u_3
inst✝ : CommRing R
P : Set R
add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P
mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P
sq : ∀ (x : R), x * x ∈ P
neg_one : -1 ∉ P
⊢ 1 ∈ P

Tactic:
simpa using sq 1

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : (↑a / ↑b)⁻¹ ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
show (a / b : K)⁻¹ = b / a by simp

Goal state after:
case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : ↑b / ↑a ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

Tactic:
have hzyclass : mk (y.val - x) hxy0 = mk (z.val - y.val) hzyne := by
    suffices ArchimedeanClass.mk (y.val - x) = .mk (z.val - y.val) by
      simpa [Subtype.ext_iff] using! this
    have : y.val - z.val = y.val - x + (x - z.val) := by abel
    rw [ArchimedeanClass.mk_sub_comm z.val y.val, this]
    refine (ArchimedeanClass.mk_add_eq_mk_left ?_).symm
    rw [ArchimedeanClass.mk_sub_comm x z.val]
    simpa using! hz (by simpa [sub_eq_zero])

Goal state after:
case refine_2
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
hzyclass : FiniteArchimedeanClass.mk (↑y - x) hxy0 = FiniteArchimedeanClass.mk (↑z - ↑y) hzyne
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : K
h : 0 ≤ mk x
⊢ 0 ≤ mk (-x)

Tactic:
mk_neg

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : K
h : 0 ≤ mk x
⊢ 0 ≤ mk x