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

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

Tactic:
calc
    (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!
      ≤ ((2 * ∑ i ∈ s, f i) ^ (∑ i ∈ s, f i) * (∑ i ∈ s, f i)!) * ∏ i ∈ s, (f i)! := by
      gcongr; exact Nat.factorial_two_mul_le _
    _ = ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! := by
      rw [mul_pow, ← prod_pow_eq_pow_sum, prod_mul_distrib]; ring
    _ ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)! := by
      gcongr
      rw [← doubleFactorial_two_mul]
      exact doubleFactorial_le_factorial _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), (eval x) p = (eval x) q

Tactic:
rintro rfl; simp only [forall_const]

Goal state after:
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✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ ({i}, single i (x i), erase i x).2.1.piecewise ({i}, single i (x i), erase i x).2.2
      ({i}, single i (x i), erase i x).1 =
    x
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q

Tactic:
classical
  simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]
  rw [Polynomial.natDegree_mul] <;> simpa [-renameEquiv_apply, EmbeddingLike.map_eq_zero_iff]

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
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c)) *
        (optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree =
    ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree

Tactic:
rw [Polynomial.natDegree_mul']

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
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).natDegree +
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree =
    ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree

case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).leadingCoeff *
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff ≠
    0
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.succ) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (tail r)}) = #(S 0 ×ˢ {r ∈ piFinset (tail S) | P r})

Tactic:
← map_consEquiv_filter_piFinset,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (tail r)}) = #(map (consEquiv α).symm.toEmbedding ({r ∈ piFinset S | P (tail r)}))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.toSyn.symm ((if c = 0 then ∅ else {d}).sup ⇑m.toSyn) = if c = 0 then 0 else d

Tactic:
split_ifs with hc

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : c = 0
⊢ m.toSyn.symm (∅.sup ⇑m.toSyn) = 0

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : ¬c = 0
⊢ m.toSyn.symm ({d}.sup ⇑m.toSyn) = d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ coeff (if c = 0 then 0 else d) ((monomial d) c) = c

Tactic:
split_ifs with hc

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : c = 0
⊢ coeff 0 ((monomial d) c) = c

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ coeff d ((monomial d) c) = c
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.Monic ((monomial d) c) ↔ c = 1

Tactic:
by
  rw [Monic, m.leadingCoeff_monomial]

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 : σ →₀ ℕ
⊢ m.toSyn (m.degree f) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d

Tactic:
unfold degree

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) ≤ m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c ≤ m.toSyn d
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 : 0 < m.toSyn d
⊢ m.toSyn (m.degree f) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d

Tactic:
unfold degree

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : 0 < m.toSyn d
⊢ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn)) < m.toSyn d ↔ ∀ c ∈ f.support, m.toSyn c < m.toSyn d
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 : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.degree f)

Tactic:
unfold degree

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
rw [← not_le, hf] at h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2

Tactic:
rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]

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

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ k + 2 ≤ m

Tactic:
apply (Nat.eq_or_lt_of_le ml).resolve_left

Goal state after:
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ ¬k.succ = m
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
(prod_normalizedFactors h0).symm.dvd_iff_dvd_right

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.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

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm ((-f).support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case hi
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal

Tactic:
aesop (add simp mul_assoc)

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

Goal state before:
pp: case hj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) ∈
      n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal

Tactic:
aesop (add simp mul_assoc)

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

Goal state before:
pp: case left_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩) =
      a

Tactic:
aesop (add simp mul_assoc)

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

Goal state before:
pp: case right_neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i * k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩) =
      a

Tactic:
aesop (add simp mul_assoc)

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

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ a ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal,
    f a.snd.1 • g a.snd.2 • h a.fst.2 =
      f
          (match a with
              | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).fst.1 •
        g
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.1 •
          h
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l * j), (l, j)⟩).snd.2

Tactic:
aesop (add simp mul_assoc)

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

Goal state before:
pp: p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : (p ^ m).factorization = (a ^ n).factorization
⊢ m = n * a.factorization p

Tactic:
rw [Nat.Prime.factorization_pow hp, Nat.factorization_pow] at this

Goal state after:
p a m n : ℕ
hp : Prime p
h : p ^ m = a ^ n
this : Finsupp.single p m = n • a.factorization
⊢ m = n * a.factorization p
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m k : ℕ
⊢ Ω (m ^ k) = k * Ω m

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
m k : ℕ
hm : m = 0
⊢ Ω (m ^ k) = k * Ω m

case neg
m k : ℕ
hm : ¬m = 0
⊢ Ω (m ^ k) = k * Ω m
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d : ℕ
⊢ d.finMulAntidiag 1 = {fun x ↦ 1}

Tactic:
by
  ext
  simp only [mem_finMulAntidiag, prod_eq_one_iff, mem_univ, forall_const, ne_eq, one_ne_zero,
    not_false_eq_true, and_true, mem_singleton]
  grind

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

Goal state before:
pp: case cons
ι : 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)
⊢ (f a).Coprime (∏ x ∈ s, f x)

Tactic:
· exact Coprime.prod_right fun i hi =>
        h (by simp) (by simp [hi]) (ne_of_mem_of_not_mem hi ha).symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2

Tactic:
· rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.2.1, h.2, gcd_mul_right,
          cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : x ≠ 0
h1 : x < 1
n : ℕ
⊢ ∑ i ∈ range n, x ^ i < (1 - x)⁻¹

Tactic:
rw [← pos_iff_ne_zero] at h0
  rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]
  · exact ⟨h0.trans h1, pow_pos h0 n⟩
  · rwa [ne_eq, tsub_eq_zero_iff_le, not_le]
  · rwa [tsub_pos_iff_lt]

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

Goal state before:
pp: case 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 (a i) < mk (a (s.min' hs))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ (mk ∘ a) i < (mk ∘ a) (s.min' hs)

Tactic:
exact hlt

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

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

Tactic:
exact hlt

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

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)

Tactic:
coe_range,

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' Set.Iio #s
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s)) ≤ ∑ x ∈ s, x

Tactic:
grw [← sum_inter_add_sum_sdiff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind

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

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)

Tactic:
coe_range,

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' Set.Iio #s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } ≤ some t

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some t

Tactic:
· exact WithBot.coe_le_coe.2 ⟨le_sup_right, inf_le_right⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some t
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
⊢ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) = {(hs.min hns, ht.min hnt)}

Tactic:
ext ⟨a, b⟩

Goal state after:
α : 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, b) ∈ mulAntidiagonal ⋯ ⋯ (hs.min hns * ht.min hnt) ↔ (a, b) ∈ {(hs.min hns, ht.min hnt)}
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ x.coeff x.order = 0 ↔ x = 0

Tactic:
by
  refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩
  rw [order_of_ne hx]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).support = (AddOpposite.unop x).support

Tactic:
rw [← addOppositeEquiv_support, AddEquiv.apply_symm_apply]

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

Goal state before:
pp: 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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : ArchimedeanClass.mk ↑a = ArchimedeanClass.mk ↑b
⊢ ArchimedeanClass.mk a = ArchimedeanClass.mk b

Tactic:
ArchimedeanClass.mk_eq_mk

Goal state after:
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
this : (∃ m, |↑b| ≤ m • |↑a|) ∧ ∃ n, |↑a| ≤ n • |↑b|
⊢ (∃ m, |b| ≤ m • |a|) ∧ ∃ n, |a| ≤ n • |b|
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
⊢ x * y ≤ z

Tactic:
grw [h1]

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ₗ z
⊢ (y ⇨ₗ z) * y ≤ z
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]

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
h✝ : toLex (ao, ac) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, ac))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

Tactic:
induction ac using FiniteArchimedeanClass.ind with | mk a ha
      induction bc using FiniteArchimedeanClass.ind with | mk b hb
      simp only [ne_eq, ofLex_toLex, FiniteArchimedeanClass.liftOrderHom_mk]
      rw [FiniteArchimedeanClass.mk_le_mk, archimedeanClassMk_le_archimedeanClassMk_iff]
      exact .inl (by simpa [ha, hb] using! h)

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ x_1 ∈ VAddAntidiagonal a ⋯,
      (x.coeff x_1.1 • ((of R).symm z).coeff x_1.2 + y.coeff x_1.1 • ((of R).symm z).coeff x_1.2) =
    ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm z).coeff ij.2 +
      ∑ ij ∈ VAddAntidiagonal a ⋯, y.coeff ij.1 • ((of R).symm z).coeff ij.2

Tactic:
simp only [sum_add_distrib]

Goal state after: