mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! = (f a + ∑ i ∈ s, f i).choose (∑ i ∈ s, f i) * (f a)! * (∑ i ∈ s, f i)!

pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!

Tactic:
Nat.add_choose_mul_factorial_mul_factorial,

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! = (f a + ∑ i ∈ s, f i)!

α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ⇑s ∉ a.support.piAntidiag n
hs'' : s.support ⊆ a.support
⊢ False

Tactic:
Finset.mem_piAntidiag,

Goal state after:
case h₁
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : ¬(a.support.sum ⇑s = n ∧ ∀ (i : σ), s i ≠ 0 → i ∈ a.support)
hs'' : s.support ⊆ a.support
⊢ False
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
⊢ ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)

Tactic:
refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_

Goal state after:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : f ∈ s.piAntidiag p.2
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)
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
⊢ p ∣ (monomial n) 1 * q

Tactic:
rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, 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.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

Tactic:
· refine ⟨⟨{ j | r j i → j ∈ p }, piecewise x₁ x { j | r j i }, x₂⟩,
      .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩ <;> simp only [piecewise_apply, Set.mem_ofPred_eq]
    · simp only [if_pos hj]
    · split_ifs with hi
      · rwa [hr i hi, if_pos hp] at hs
      · assumption
    · ext1 j
      simp only [piecewise_apply, Set.mem_ofPred_eq]
      split_ifs with h₁ h₂ <;> try rfl
      · rw [hr j h₂, if_pos (h₁ h₂)]
      · rw [Classical.not_imp] at h₁
        rw [hr j h₁.1, if_neg h₁.2]

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) < degree (ofDegLex b)
hbc : degree (ofDegLex b) < degree (ofDegLex c)
⊢ degree (ofDegLex a) < degree (ofDegLex c)

Tactic:
exact lt_trans hab hbc

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a b c : DegLex (α →₀ ℕ)), a < b → b < c → a < c

Tactic:
by
    intro a b c hab hbc
    simp only [lt_iff] at hab hbc ⊢
    rcases hab with (hab | hab)
    · rcases hbc with (hbc | hbc)
      · left; exact lt_trans hab hbc
      · left; exact lt_of_lt_of_eq hab hbc.1
    · rcases hbc with (hbc | hbc)
      · left; exact lt_of_eq_of_lt hab.1 hbc
      · right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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 : MvPolynomial σ R
d : σ →₀ ℕ
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f = 0

Tactic:
rw [← not_le] at hd

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
⊢ coeff d f = 0
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
hf : m.Monic f
hg : m.Monic g
⊢ m.Monic (f * g)

Tactic:
by
  nontriviality R
  suffices m.leadingCoeff f * m.leadingCoeff g = 1 by
    rw [Monic, MonomialOrder.leadingCoeff,
      degree_mul_of_mul_leadingCoeff_ne_zero, coeff_mul_of_degree_add, this]
    rw [this]
    exact one_ne_zero
  rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
this : Finsupp.cons k (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p'.leadingCoeff)) ∈ p.support
⊢ k ≤ degreeOf 0 p

Tactic:
simpa using monomial_le_degreeOf 0 this

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) ≠ m.toSyn (m.degree f)

Tactic:
by_contra! h'

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
h' : m.toSyn (m.degree (f - m.leadingTerm f)) = m.toSyn (m.degree f)
⊢ False
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
refine ⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩
  rcases h with ⟨p, pp, h⟩
  rw [isPrimePow_nat_iff]
  rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ordProj_dvd n p) h] at hn ⊢
  refine ⟨p, n.factorization p, pp, ?_, by simp⟩
  contrapose! hn
  simp [Nat.le_zero.1 hn]

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

Goal state before:
pp: case mpr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn₀)

Goal state after:
case mpr.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

case mpr.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ ∏ p ∈ n.primeFactors, p ∣ k ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · grw [← Nat.primeFactors_mono h hk, primeFactors_prod_primeFactors]
  · grw [← k.prod_primeFactors_dvd, Finset.prod_dvd_prod_of_subset _ _ _ h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ ∏ p ∈ x.primeFactors ∪ y.primeFactors, f p = (∏ p ∈ x.primeFactors, f p) * ∏ p ∈ y.primeFactors, f p

Tactic:
← prod_union hxy.disjoint_primeFactors

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ ∏ p ∈ x.primeFactors ∪ y.primeFactors, f p = ∏ x ∈ x.primeFactors ∪ y.primeFactors, f x
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
⊢ f i ∣ n

Tactic:
mem_finMulAntidiag

Goal state after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m → f ∈ d.finMulAntidiag m

Tactic:
mem_finMulAntidiag

Goal state after:
case mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i, f i = m → ∏ i, f i = m ∧ m ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k

Tactic:
mem_finMulAntidiag

Goal state after:
case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i, a i = n ∧ n ≠ 0) ∧ a i = k
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f ↦ f i) (d.finMulAntidiag n) = n.divisors

Tactic:
by
  ext k
  simp only [mem_image, ne_eq, mem_divisors]
  constructor
  · rintro ⟨f, hf, rfl⟩
    exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩
  · simp_rw [mem_finMulAntidiag]
    rintro ⟨⟨r, rfl⟩, hn⟩
    have hs : Nontrivial (Fin d) := by
      rw [Fin.nontrivial_iff_two_le]
      obtain rfl | hd' := eq_or_ne d 0
      · exact i.elim0
      lia
    obtain ⟨i', hi_ne⟩ := exists_ne i
    use fun j => if j = i then k else if j = i' then r else 1
    simp only [ite_true, and_true]
    rw [← Finset.mul_prod_erase (h := mem_univ i),
      ← Finset.mul_prod_erase (a := i')]
    · simp_all
    exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩

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

Goal state before:
pp: d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∃! i, p ∣ f i

Tactic:
mem_finMulAntidiag

Goal state after:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (f * ↑zeta) n = ∑ n ∈ Ioc 0 N, f n * ↑(N / n)

Tactic:
rw [sum_Ioc_mul_eq_sum_sum]

Goal state after:
R : Type u_2
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, f n * ∑ m ∈ Ioc 0 (N / n), ↑zeta m = ∑ n ∈ Ioc 0 N, f n * ↑(N / n)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ d.primeFactorsPiBij n f hf ∈ d.finMulAntidiag n

Tactic:
mem_finMulAntidiag

Goal state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ i, d.primeFactorsPiBij n f hf i = n ∧ n ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
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
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial
            ((m.degree ((monomial d₁) c₁) + m.degree p₁) ⊔ (m.degree ((monomial d₂) c₂) + m.degree p₂) -
                (m.degree ((monomial d₁) c₁) + m.degree p₁) +
              d₁))
          (m.leadingCoeff ((monomial d₂) c₂) * m.leadingCoeff p₂ * c₁) *
        p₁ -
      (monomial
            ((m.degree ((monomial d₁) c₁) + m.degree p₁) ⊔ (m.degree ((monomial d₂) c₂) + m.degree p₂) -
                (m.degree ((monomial d₂) c₂) + m.degree p₂) +
              d₂))
          (m.leadingCoeff ((monomial d₁) c₁) * m.leadingCoeff p₁ * c₂) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂

Tactic:
m.leadingCoeff_monomial,

Goal state after:
σ✝ : 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
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial
            ((m.degree ((monomial d₁) c₁) + m.degree p₁) ⊔ (m.degree ((monomial d₂) c₂) + m.degree p₂) -
                (m.degree ((monomial d₁) c₁) + m.degree p₁) +
              d₁))
          (c₂ * m.leadingCoeff p₂ * c₁) *
        p₁ -
      (monomial
            ((m.degree ((monomial d₁) c₁) + m.degree p₁) ⊔ (m.degree ((monomial d₂) c₂) + m.degree p₂) -
                (m.degree ((monomial d₂) c₂) + m.degree p₂) +
              d₂))
          (c₁ * m.leadingCoeff p₁ * c₂) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a ∈ finMulAntidiag 3 n

Tactic:
mem_finMulAntidiag

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n ∧ n ≠ 0
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
A : MulArchimedeanClass M
⊢ A ≤ mk 1

Tactic:
induction A using ind with

Goal state after:
case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ mk a ≤ mk 1
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
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
A B : MulArchimedeanClass M
hle : A ≤ B
⊢ lift f ⋯ A ≤ lift f ⋯ B

Tactic:
induction A using ind with

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B
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
inst✝ : MulArchimedean M
A B : FiniteMulArchimedeanClass M
⊢ A = B

Tactic:
induction A using ind with

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
inst✝ : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B
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
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
A B : FiniteMulArchimedeanClass M
hAB : A ≤ B
⊢ lift f ⋯ A ≤ lift f ⋯ B

Tactic:
induction A using ind with

Goal state after:
case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ n ≤ ⌈r⌉ₑ ↔ ↑n - 1 < r

Tactic:
lift n to ℕ using hn
  cases r
  · simp only [ceil_top, le_top, toENNReal_coe, true_iff]
    norm_cast
    exact ENNReal.coe_lt_top
  · simp only [ne_eq, Nat.cast_eq_zero, ceil_coe, Nat.cast_le, toENNReal_coe] at hn₀ ⊢
    norm_cast
    rw [← Nat.add_one_le_ceil_iff, Nat.sub_add_cancel]
    lia

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ ⌊↑(Int.negOfNat n) * ⅟↑d⌋₊ = ↑0

Tactic:
Nat.cast_zero,

Goal state after:
R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
n d : ℕ
hd : Invertible ↑d
⊢ ⌊↑(Int.negOfNat n) * ⅟↑d⌋₊ = 0
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
⊢ Subgroup.genLTOne H ∈ H

Tactic:
nth_rewrite 1 [← H.genLTOne_zpowers_eq_top]

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
⊢ Subgroup.genLTOne H ∈ Subgroup.zpowers (Subgroup.genLTOne H)
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = ↑g
⊢ x.coeff g ≠ 0

Tactic:
have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = ↑g
h : x.orderTop ≠ ⊤
⊢ x.coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).orderTop = y.orderTop

Tactic:
by
  simpa [← map_add, ← AddOpposite.op_add, hxy] using orderTop_add_eq_left
    (x := addOppositeEquiv.symm (.op y))
    (y := addOppositeEquiv.symm (.op x))

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

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

Tactic:
by
  rw [u.inv_mul_le_iff, mul_one]

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

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * x ≤ z

Tactic:
grw [h1]
    simp_all only [rightMulResiduation, mul_sSup_distrib, Set.mem_ofPred_eq,
      iSup_le_iff, implies_true]

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✝³ x✝² x✝¹ x✝ : R
hx : mk x✝³ = mk x✝²
hy : mk x✝¹ = mk x✝
⊢ mk (x✝³ * x✝¹) = mk (x✝² * x✝)

Tactic:
exact (mk_mul_le_of_le hx.le hy.le).antisymm (mk_mul_le_of_le hx.ge hy.ge)

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
n : ℕ
x y : R
h : mk x = mk y
⊢ mk (x ^ n) = mk (y ^ n)

Tactic:
induction n with
    | zero => simp
    | succ n IH => simp_rw [pow_succ, mk_mul, IH, h]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

pp: case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : ¬f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0

Tactic:
· exact mul_eq_zero_of_left h (f (y.coeff gh.2))

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
x y : R⟦Γ⟧
x✝ : Γ
gh : Γ × Γ
hgh : ¬x.coeff gh.1 = 0 ∧ ¬y.coeff gh.2 = 0 ∧ gh.1 + gh.2 = x✝
hz : ¬f (x.coeff gh.1) = 0 → f (y.coeff gh.2) = 0
h : ¬f (x.coeff gh.1) = 0
⊢ f (x.coeff gh.1) * f (y.coeff gh.2) = 0