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

Goal state before:
pp: x : ℕ
l : List ℕ
⊢ (x :: l).multinomial = (x + l.sum).choose x * l.multinomial

Tactic:
by
  simp only [multinomial]
  rw [Finsupp.multinomial_update 0 (x :: l).toFinsupp]
  congr 1
  · congr
    exact List.toFinsupp_sum (x :: l)
  let succEmb : ℕ ↪ ℕ := addRightEmbedding 1
  have : (Finsupp.single 0 x + l.toFinsupp.embDomain succEmb).update 0 0 =
    (l.toFinsupp.embDomain succEmb).update 0 0 := by
    ext i
    by_cases hi : i = 0
    · simp [hi]
    · simp [Finsupp.update_apply, if_neg hi, Finsupp.single_eq_of_ne hi]
  have h (x) : (l.toFinsupp.embDomain succEmb) (x + 1) = l[x]?.getD 0 := by
    rw [Finsupp.embDomain_apply, dif_pos ⟨x, by simp [succEmb]⟩]
    simp [succEmb]
  simp [toFinsupp_cons_eq_single_add_embDomain, Finsupp.multinomial_eq,
    succEmb, this, Nat.multinomial, h]

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inr.fst
α : 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)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(b, d)

Tactic:
rw [Sym2.eq_swap]
    exact iha d rd ⟨b, hb⟩

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

Goal state before:
pp: case intro
ι : 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
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hs : s k (x k) (if h : i = k then Eq.recOn h a else 0)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
split_ifs at hs with hik

Goal state after:
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
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : i = k
hs : s k (x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x

case neg
ι : 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
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hik : ¬i = k
hs : s k (x k) 0
⊢ Acc (DFinsupp.Lex r s) x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex

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

Tactic:
simp [hf]

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

Goal state before:
pp: case inr.insert
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ degreeOf n (∏ i ∈ insert a s, f i) = ∑ i ∈ insert a s, degreeOf n (f i)

Tactic:
simp [a_not_mem, not_false_eq_true, prod_insert, sum_insert, degreeOf_mul_eq ha
        (by rw [prod_ne_zero_iff]; exact hs), ih hs]

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
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + g) = m.leadingCoeff f

Tactic:
simp only [leadingCoeff, m.degree_add_of_lt h, coeff_add, coeff_eq_zero_of_lt h, add_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
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
this : m.toSyn (m.degree g) < m.toSyn d
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
coeff_eq_zero_of_lt this,

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hf]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hf]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f

Tactic:
simp [hf]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ (monomial (m.degree p)) (m.leadingCoeff p) = (monomial (m.degree q)) (m.leadingCoeff q) ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

Tactic:
monomial_eq_monomial_iff

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ m.Monic p

Tactic:
simp [Subsingleton.eq_one (α := MvPolynomial σ R)]

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

Goal state before:
pp: case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
simp only [h, ↓reduceDIte]

Goal state after:
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp none
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
simp only [h, ↓reduceDIte]

Goal state after:
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp (if k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f : MvPolynomial σ R
inst✝ : Decidable (f = 0)
hf : f = 0
⊢ WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max =
    if f = 0 then ⊥ else ↑(m.toSyn.symm (f.support.sup ⇑m.toSyn))

Tactic:
simp [hf]

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

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n

Tactic:
exact this.2.1

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
simp [hf]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x ^ k.succ = (f.pmul (f.ppow k)) x

Tactic:
_root_.pow_succ'

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k.succ = ((f.ppow k).pmul f) x

Tactic:
_root_.pow_succ

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k * f x = ((f.ppow k).pmul f) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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 : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.1.divisorsAntidiagonal, f x.snd.1 • g x.snd.2 • h x.fst.2 =
    ∑ x ∈ n.divisorsAntidiagonal.sigma fun a ↦ a.2.divisorsAntidiagonal, f x.fst.1 • g x.snd.1 • h x.snd.2

Tactic:
apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc)

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

Goal state before:
pp: case refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∈ S

Tactic:
simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]
    refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring

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

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n

Tactic:
by
  simp only [isPrimePow_iff_unique_prime_dvd]
  apply existsUnique_congr
  simp +contextual [Nat.prime_iff, Prime.dvd_pow_iff_dvd, hk]

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

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

Tactic:
simp [hf]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h✝ : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
h : t ⊆ Finset.range (m + 1)
⊢ n' • r ≤ ∑ i ∈ t, r

Tactic:
sum_eq_card_nsmul (fun _ _ ↦ rfl),

Goal state after:
case h
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h✝ : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
m : ℕ
hm : m ∈ upperBounds ↑t
h : t ⊆ Finset.range (m + 1)
⊢ n' • r ≤ #t • r
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ {n | ω ∈ s n}.Infinite ↔ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop

Tactic:
infinite_iff_tendsto_sum_indicator_atTop h,

Goal state after:
α : Type u_1
R : Type u_2
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n ↦ ∑ k ∈ Finset.range n, {n | ω ∈ s n}.indicator (fun x ↦ r) k) atTop atTop ↔
    Tendsto (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun x ↦ r) ω) atTop atTop
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
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ b1 * b2 = n * m

Tactic:
rw [mul_comm n m, h.1]

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

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
this : (∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ) → ∃ n, |val b|ₘ ≤ |val a|ₘ ^ n
⊢ (∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ) ↔ (∃ n, |val b|ₘ ≤ |val a|ₘ ^ n) ∧ ¬∃ n, |val a|ₘ ≤ |val b|ₘ ^ n

Tactic:
simpa using this

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_lcm : f (x.lcm y) ≠ 0
⊢ f (x.gcd y) = f x * f y / f (x.lcm y)

Tactic:
by
  rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]

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
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
this : a⁻¹ < b / a
⊢ 1 < b

Tactic:
simpa using this

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f✝ : ι →₀ β
a _a : α
ha : 0 < _a
f _g : ι →₀ β
i : ι
⊢ ((fun x ↦ _a • x) f) i ≤ _g i ↔ f i ≤ ((fun x ↦ mapRange (fun x ↦ x ⌊/⌋ _a) ⋯ x) _g) i

Tactic:
by
    simpa only [coe_smul, Pi.smul_apply, mapRange_apply] using gc_floorDiv_smul ha (f i) _

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
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s < t
⊢ { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ } <
    { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ t}, upper' := ⋯ }

Tactic:
lt_iff_le_not_ge

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s ≤ t ∧ ¬t ≤ s
⊢ { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ } ≤
      { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ t}, upper' := ⋯ } ∧
    ¬{ carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ t}, upper' := ⋯ } ≤
        { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ }
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
exact map_add_left_Icc _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
by
  simp_rw [add_comm _ c]
  exact map_add_left_Ioo _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Interval α
⊢ ↑(dual s) = ⇑ofDual ⁻¹' ↑s

Tactic:
cases s with

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ lowerBounds s₁
⊢ s ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥

Tactic:
cases s with

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

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup E₁
inst✝⁶ : PartialOrder E₁
inst✝⁵ : IsOrderedAddMonoid E₁
inst✝⁴ : AddCommGroup E₂
inst✝³ : PartialOrder E₂
inst✝² : IsOrderedAddMonoid E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x
a b : E₁
hab : 0 ≤ b - a
this : 0 ≤ f (b - a)
⊢ 0 ≤ f.toFun b - f.toFun a

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inl.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
obtain rfl := hb.antisymm (ha.trans hab)

Goal state after:
case inl.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a : G
ha : 0 ≤ a
hab : a ≤ 0
hb : 0 ≤ 0
⊢ ↑(#(Ico 0 (a + 0))) - ↑(#(Ico 0 (-(a + 0)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
⊢ Function.Bijective ⇑(orderAddMonoidHom G)

Tactic:
by
  refine ⟨orderAddMonoidHom_strictMono.injective, ?_⟩
  suffices 1 ∈ (orderAddMonoidHom G).range by
    obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩
  have ⟨a, ha⟩ := exists_zero_lt (α := G)
  obtain ⟨b, hb⟩ := exists_covBy_of_wellFoundedLT (α := Icc 0 a) (a := ⟨0, by simpa using! ha.le⟩)
    (fun H ↦ ha.not_ge (@H ⟨a, by simpa using! ha.le⟩ ha.le))
  use b.1
  have : 0 ≤ b.1 := hb.1.le
  suffices Ico 0 b.1 = {0} by simpa [orderAddMonoidHom, addMonoidHom, this]
  ext x
  simp only [mem_Ico, mem_singleton]
  constructor
  · rintro ⟨h₁, h₂⟩
    by_contra hx'
    have := b.2
    simp only [Finset.mem_Icc] at this
    exact hb.2 (c := ⟨x, by simpa [h₁] using! h₂.le.trans this.2⟩)
      (lt_of_le_of_ne h₁ (by simpa using! Ne.symm hx')) h₂
  · rintro rfl
    simpa using! hb.1

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
x : α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * ⨆ i, f i = ⨆ i, x * f i

Tactic:
rw [iSup, mul_sSup_distrib, iSup_range]

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
u : ArchimedeanStrata K M
⊢ iSupIndep u.stratum'

Tactic:
by
  apply (iSupIndep_map_orderIso_iff (Submodule.mapIic u.baseDomain)).mp
  apply iSupIndep.of_coe_Iic_comp
  convert! u.iSupIndep_stratum
  ext1 c
  simpa using! le_iSup _ _

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
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
c : FiniteArchimedeanClass M
hc : c ∈ ↑f.support
d : FiniteArchimedeanClass M
hd : d ∈ ↑f.support
h : c < d
⊢ ↑(f d) ≠ 0

Tactic:
simpa using! hd

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ x * (y + z) = x * y + x * z

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (HahnModule.of R).symm (x • (HahnModule.of R) (y + z)) =
    (HahnModule.of R).symm (x • (HahnModule.of R) y) + (HahnModule.of R).symm (x • (HahnModule.of R) z)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (x + y) * z = x * z + y * z

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (HahnModule.of R).symm ((x + y) • (HahnModule.of R) z) =
    (HahnModule.of R).symm (x • (HahnModule.of R) z) + (HahnModule.of R).symm (y • (HahnModule.of R) z)
Module: Mathlib.Algebra.Order.Ring.Archimedean

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

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge_of_mk_nonneg hx
  refine ⟨n + 1, hn.trans_lt ?_⟩
  simp

Goal state after: