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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α → ℕ
s t : Finset α
hf : ∀ a ∈ s \ t, f a = 0
hg : ∀ a ∈ t \ s, g a = 0
hfg : ∀ a ∈ s ∩ t, f a = g a
⊢ multinomial s f = multinomial t g

Tactic:
by
  rw [← Nat.mul_right_inj (prod_ne_zero_iff.mpr (fun x _ ↦ factorial_ne_zero (g x))),
    multinomial_spec, prod_congr_of_eq_on_inter (g := fun a ↦ (f a)!) (s₂ := s) (by aesop)
    (by aesop) (by aesop), multinomial_spec s f]
  congr 1
  exact sum_congr_of_eq_on_inter (by grind) (by grind) (by grind)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ i = j ∧ ¬1 = 0 ↔ i = j

Tactic:
reduceCtorEq,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ i = j ∧ ¬False ↔ i = j
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
i : σ
p r : MvPolynomial σ R
h✝ : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : n i ≠ 0
⊢ Finsupp.single i 1 ≤ n

Tactic:
simpa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)

Tactic:
eq_modMonomial_single_iff

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ ∀ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support, n i = 0

case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf : IsUnit ((expand p) f)
⊢ IsUnit f

Tactic:
rw [MvPolynomial.isUnit_iff] at hf ⊢

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : MvPolynomial σ R
hf : IsUnit (coeff 0 ((expand p) f)) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i ((expand p) f))
⊢ IsUnit (coeff 0 f) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i f)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction hb with

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
induction hb with

Goal state after:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c < lex.toSyn d ↔ c default < d default

Tactic:
by
  simp only [MonomialOrder.lex_lt_iff, Finsupp.Lex.lt_iff_of_unique, ofLex_toLex]

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

Goal state before:
pp: case pos.inl
ι : 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 : ι
x : Π₀ (i : ι), α i
j : ι
hj : j ∈ x.support
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y j → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y j → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α j
ha : ∀ (y : α j), s j y a → Acc (DFinsupp.Lex r s) (single j y)
hr : ∀ (j_1 : ι), r j_1 j → x j_1 = (single j a) j_1
hs : s j (x j) (Eq.recOn ⋯ a)
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

pp: case pos.inr
ι : 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
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
· exact ha _ hs

Goal state after:
case pos.inr
ι : 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
⊢ Acc (DFinsupp.Lex r s) (single j (x j))
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J ∉ s}
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ ε' * B J

Tactic:
by
      rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
      refine Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ)
        fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)
      convert! hπδ.1 J hJ using 3; exact (if_neg hJs).symm

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

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

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

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

Goal state before:
pp: case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

Tactic:
rw [not_imp_not]
    intro hf
    rw [hf, leadingCoeff_zero]

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
f g : MvPolynomial σ R
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases! +distrib h : f = 0 ∨ g = 0

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
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
⊢ Finsupp.cons k (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p'.leadingCoeff)) ∈ p.support

Tactic:
← mem_support_coeff_finSuccEquiv,

Goal state after:
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
⊢ ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p'.leadingCoeff) ∈ (((finSuccEquiv R n) p).coeff k).support
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ f * dirichletInverse (⇑f) hf = 1

Tactic:
self_mul_dirichletInverse

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ 1 = 1
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n.primeFactorsList.Subperm (p ^ n.factorization p).primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case succ
n : ℕ
h : Ω (n + 1) = 1
⊢ Nat.Prime (n + 1)

Tactic:
rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩

Goal state after:
case succ
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime (n + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    (match a with
      | ((i, j), k, l) => (i * k, j * l)) ∈
      (m * n).divisorsAntidiagonal

pp: case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

pp: case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.SurjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) =
      f
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).1 *
        g
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).2

Tactic:
· rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
    simp only [mem_divisorsAntidiagonal, Ne, mem_product] at h
    rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
    simp only [mem_divisorsAntidiagonal, mul_eq_zero, Ne]
    constructor
    · ring
    rw [mul_eq_zero] at *
    exact not_or_intro ha hb

Goal state after:
case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.SurjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) =
      f
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).1 *
        g
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).2
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
sum_Ioc_zeta

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

Goal state before:
pp: n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ f a ha ∈ n.divisors ×ˢ n.divisors ∧
    match f a ha with
    | (x, y) => x.lcm y = n

Tactic:
Finset.mem_product,

Goal state after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ ((f a ha).1 ∈ n.divisors ∧ (f a ha).2 ∈ n.divisors) ∧
    match f a ha with
    | (x, y) => x.lcm y = n
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 ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) + d₁ - (d₁ + m.degree p₁))) (c₁ * c₂ * m.leadingCoeff p₂) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) + d₂ - (d₂ + m.degree p₂))) (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂ =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁)) (c₁ * c₂ * m.leadingCoeff p₂) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₂)) (c₁ * c₂ * m.leadingCoeff p₁) * p₂

Tactic:
add_comm d₁,

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 p₁ + d₁) ⊔ (d₂ + m.degree p₂) + d₁ - (m.degree p₁ + d₁))) (c₁ * c₂ * m.leadingCoeff p₂) * p₁ -
      (monomial ((m.degree p₁ + d₁) ⊔ (d₂ + m.degree p₂) + d₂ - (d₂ + m.degree p₂))) (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂ =
    (monomial ((m.degree p₁ + d₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁)) (c₁ * c₂ * m.leadingCoeff p₂) * p₁ -
      (monomial ((m.degree p₁ + d₁) ⊔ (d₂ + m.degree p₂) - m.degree p₂)) (c₁ * c₂ * m.leadingCoeff p₁) * p₂
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: 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

Tactic:
hs.mem_toFinset

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 ∈ s → x ∈ Finset.range n
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: 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

Tactic:
hs.mem_toFinset

Goal state after:
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 ∉ s → 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✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

Tactic:
wlog! +distrib H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, leadingTerm, sPolynomial_monomial_mul, degree_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
by
  rcases le_or_gt m n with (hmn | hmn)
  · rw [geom_sum_Ico' h'x.ne hmn]
    apply div_le_div₀ (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
    simpa using pow_nonneg hx _
  · rw [Ico_eq_empty, sum_empty]
    · apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le
    · simpa using hmn.le

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

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 ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ {x | σ⁻¹ x ≠ x} ⊆ ↑s

Tactic:
simp [set_support_symm_eq, hσ]

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

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ = 0 ↔ r < 1

Tactic:
by simp [← nonpos_iff_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
⊢ g1 = g2

Tactic:
by
  rcases (Subgroup.zpowers g2).bot_or_nontrivial with (h' | h')
  · rw [h'] at h
    simp_all only [Subgroup.zpowers_eq_bot]
  · have h1 : IsCyclic ↥(Subgroup.zpowers g2) := by
      rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]; use g2
    have h2 : Nontrivial ↥(Subgroup.zpowers g1) := by rw [h]; exact h'
    have h3 : IsCyclic ↥(Subgroup.zpowers g1) := by rw [h]; exact h1
    simp only [(Subgroup.zpowers g2).genLTOne_unique hg1 h]
    simp only [← h]
    simp only [(Subgroup.zpowers g1).genLTOne_unique hg2 h.symm]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c

Tactic:
mem_range

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x < #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)

Tactic:
mem_range

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x < #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t s : NonemptyInterval α
⊢ s⁻¹⁻¹ = s

Tactic:
by apply NonemptyInterval.ext; exact inv_inv _

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

Goal state before:
pp: case some
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ - -some s = some s

Tactic:
exact congr_arg WithBot.some (neg_neg _)

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ hs.min hns ∈ s ∧ ht.min hnt ∈ t ∧ hs.min hns * ht.min hnt = hs.min hns * ht.min hnt