mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((p.1 + p.2).choose p.1) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (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) ⋯)

Tactic:
congr 2

Goal state after:
case cons.e_a.e_a
α : 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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((p.1 + p.2).choose p.1) = ↑(n.choose p.1)

case cons.e_a.e_a
α : 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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) = ↑(multinomial s f)

case cons.e_a.e_a
α : 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 : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯ = s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton R
⊢ ∃ m, m ≤ n

Tactic:
refine ⟨n, le_refl n⟩

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ ∀ (d : ℕ) (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

Tactic:
intro d

Goal state after:
case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
⊢ ∀ (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
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
inst✝ : DecidableEq σ
hp : p ≠ 0
⊢ ((expand p) φ).support = Finset.image (fun x ↦ p • x) φ.support

Tactic:
refine (support_expand_subset φ).antisymm ?_
  simp [Finset.image_subset_iff, hp]

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

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

Tactic:
congr 2

Goal state after:
case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose x * (m.sum + m'.sum).choose m.sum =
    (x + (m.sum + m'.sum)).choose (x + m.sum) * (x + m.sum).choose x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : 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 = ((fun x ↦ x.2.1.piecewise x.2.2 x.1) (p, x₁, x₂)) j
hs : s i (x i) (((fun x ↦ x.2.1.piecewise x.2.2 x.1) (p, x₁, 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:
simp_rw [piecewise_apply] at hs hr

Goal state after:
ι : 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
hs : s i (x i) (if i ∈ p then x₁ i else 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.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
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
h : r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
rw [hr j h, single_eq_of_ne hij, single_zero]
      exact Lex.acc_zero hbot

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree

Tactic:
by_cases hf : f = 0
  · simp [hf]
  apply le_antisymm
  · exact le_totalDegree (degLex.degree_mem_support hf)
  · unfold MvPolynomial.totalDegree
    apply Finset.sup_le
    intro b hb
    exact DegLex.monotone_degree (degLex.le_degree hb)

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (init r)}) = #(S (last n)) * #({r ∈ piFinset (init S) | P r})

Tactic:
rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d) c) = c

Tactic:
simp only [leadingCoeff, degree_monomial]
  split_ifs with hc <;> simp [hc]

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
⊢ ∀ (a : σ →₀ ℕ), a ∈ f.support → m.toSyn a ≤ m.toSyn 0 ↔ a ∈ f.support → ∀ (x : σ), a x = 0

Tactic:
intro d

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d ∈ f.support → m.toSyn d ≤ m.toSyn 0 ↔ d ∈ f.support → ∀ (x : σ), d x = 0
Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Goal state before:
pp: x y : ℤ
⊢ |x| < |y| ↔ x.natAbs < y.natAbs

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))
⊢ m.toSyn (m.degree p) < m.toSyn (m.degree p')

Tactic:
wlog! hq : q ≠ 0

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    {p p' q : MvPolynomial σ R},
    p ≠ 0 →
      m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q)) → q ≠ 0 → m.toSyn (m.degree p) < m.toSyn (m.degree p')
hq : q = 0
⊢ m.toSyn (m.degree p) < m.toSyn (m.degree p')

σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommSemiring R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))
hq : q ≠ 0
⊢ m.toSyn (m.degree p) < m.toSyn (m.degree p')
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
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.leadingCoeff f ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
classical
  by_cases! h0 : f = 0 ∨ g = 0
  · rcases h0 with h0 | h0 <;> simp [h0]
  suffices f * g ≠ 0 by simp [withBotDegree_eq, m.degree_mul_of_left_mem_nonZeroDivisors hf, *]
  apply mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors at hf
  rw [mem_nonZeroDivisors_iff_left] at hf
  tauto

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

Goal state before:
pp: case mpr
n : ℕ
this : n.MinSqFacProp n.minSqFac
H : n.minSqFac = none
⊢ Squarefree n

Tactic:
rwa [H] at this

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
  by_cases h0 : f * g = 0
  · simp [h0]
  simp [m.withBotDegree_eq_coe_degree_iff f |>.mpr (by grind),
    m.withBotDegree_eq_coe_degree_iff g |>.mpr (by grind),
    m.withBotDegree_eq_coe_degree_iff _ |>.mpr h0, ← WithBot.coe_add,
    m.toSyn_degree_mul_le]

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ x = y

Tactic:
← Finset.val_inj,

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ x.val = y.val
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
⊢ m.toSyn (m.degree (f - g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
sub_eq_add_neg

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
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
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f - g) = m.degree f

Tactic:
sub_eq_add_neg

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f
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
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f - g) = m.leadingCoeff f

Tactic:
sub_eq_add_neg

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f
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
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : m.degree f ∈ (f - m.leadingTerm f).support
⊢ False

Tactic:
mem_support_iff

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
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : coeff (m.degree f) (f - m.leadingTerm f) ≠ 0
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

Tactic:
by
  ext
  simp only [pmul_apply, mul_assoc]

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

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (if n = 1 then ⅟(f 1)
    else
      -⅟(f 1) *
        ∑ d,
          have this := ⋯;
          f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
if_neg hn1

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (-⅟(f 1) *
      ∑ d,
        have this := ⋯;
        f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f (l / d) = f l / f d

Tactic:
by
  apply (div_eq_of_eq_mul hd ..).symm
  rw [← hf.right hl, Nat.div_mul_cancel hdl]

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

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, True ∧ ⟨(↑a).1, ⋯⟩ = x.1 ∧ ⟨(↑a).2, ⋯⟩ = x.2) ↔ x.1 * x.2 = n

Tactic:
true_and,

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, ⟨(↑a).1, ⋯⟩ = x.1 ∧ ⟨(↑a).2, ⋯⟩ = x.2) ↔ x.1 * x.2 = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
⊢ a = b

Tactic:
obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
  have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
    rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
  have hab2 : a 2 = b 2 := by
    rw [← mul_right_inj' <| mul_ne_zero (ne_zero_of_mem_finMulAntidiag ha 0)
      (ne_zero_of_mem_finMulAntidiag ha 1)]
    exact hprods
  have hab0 : a 0 = b 0 := by
    rw [hab2] at hfab2
    exact (mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2;
  have hab1 : a 1 = b 1 := by
    rw [hab0] at hfab1
    exact (mul_right_inj' <| ne_zero_of_mem_finMulAntidiag hb 0).mp hfab1;
  funext i; fin_cases i <;> assumption

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

Goal state before:
pp: case h.fst
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ {x ∈ n.divisors ×ˢ n.divisors | x.1.lcm x.2 = n}
g : ℕ := ⋯
a : Fin (succ 0).succ.succ → ℕ := ⋯
ha : a ∈ finMulAntidiag 3 n
⊢ g ∣ b.1

Tactic:
apply Nat.gcd_dvd_left

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Field β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}

Tactic:
cutMap,

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Field β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
q : ℚ
⊢ Rat.cast '' {t | ↑t < ↑q} = Rat.cast '' {r | ↑r < ↑q}
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  (∀ b_1 ∈ B, m.toSyn (m.degree (g b_1)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
hd : ∀ a ∈ B, m.toSyn (m.degree (g a)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 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:
use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0

Goal state after:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
h :
  (∀ b_1 ∈ B, m.toSyn (m.degree (g b_1)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
hd : ∀ a ∈ B, m.toSyn (m.degree (g a)) = m.toSyn (m.degree (g b)) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ ∑ b ∈ insert b B, g b =
    ∑ b₁ ∈ insert b B,
      ∑ b₂ ∈ insert b B, (fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0) b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
⊢ ∀ (x : α), (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
intro x
        obtain h | rfl | h := lt_trichotomy x 0
        · convert! this (-x) (neg_pos.2 h) using 1
          · rw [neg_mul, mul_neg, neg_neg]
          · simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
        · simp only [mul_zero, map_zero]
        · exact this x h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun p k ↦ f (p ^ k)) = n.factorization.prod fun p k ↦ g (p ^ k)

Tactic:
exact prod_congr rfl fun p hp ↦ h p _ (prime_of_mem_primeFactors hp)

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

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
this : i + 1 = i
⊢ f i ≤ (Finset.Iio i).sup f ⊔ (partialSups f) i

Tactic:
apply le_trans (le_partialSups _ _) le_sup_right

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 (s.min' hs)) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
congr 2

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)
⊢ s.min' hs = (Finset.cons i s hi).min' ⋯
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

pp: case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
· simp [ha]

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
obtain hab | hba := le_total a (b - 1)⁻¹
  · calc
      ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Goal state after: