mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
refine ⟨hip, ?_⟩

Goal state after:
case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ p.divMonomial (Finsupp.single i 1) ∣ q
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, X i ^ 0 = 1

Tactic:
· simp

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

Goal state before:
pp: case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ p ∣ (monomial n) 1 * q

Tactic:
hp,

Goal state after:
case inr.succ.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
x✝ : ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m) 1 * r
⊢ (monomial m) 1 * r ∣ (monomial n) 1 * q
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : m ∈ ((expand p) φ).support
⊢ p ∣ m i

Tactic:
support_expand_subset,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
m : σ →₀ ℕ
i : σ
h : m ∈ Finset.image (fun x ↦ p • x) φ.support
⊢ p ∣ m i
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: case C
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (C a)) =
      eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (C a)

pp: case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

pp: case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)

Tactic:
· simp

Goal state after:
case add
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) q →
        Polynomial.eval x (eval₂ f g (p + q)) =
          eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p + q)

case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p →
      Polynomial.eval x (eval₂ f g (p * X n)) =
        eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ) l l'
⊢ l.multinomial = l'.multinomial

Tactic:
induction h with
  | nil => simp
  | @cons x l l' hl hl' => simp [List.multinomial_cons, hl', hl.sum_nat]
  | @swap x y l =>
    simp only [List.multinomial_cons, ← mul_assoc, List.sum_cons]
    rw [← Nat.choose_symm (Nat.le_add_right y _), add_tsub_cancel_left]
    rw [add_left_comm, Nat.choose_mul (Nat.le_add_right _ _), add_tsub_cancel_left]
    simp [← Nat.choose_symm (Nat.le_add_right _ _), add_tsub_cancel_left]
  | @trans l l' l'' h h' ih ih' => rw [ih, ih']

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))).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

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))).leadingCoeff *
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff ≠
    0

Tactic:
· simp

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))).leadingCoeff *
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff ≠
    0
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.degree ((monomial d) c) = if c = 0 then 0 else d

Tactic:
by
  simp only [degree, support_monomial]
  split_ifs with hc <;> simp

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f = 0

Tactic:
rw [← not_le] at hd
  by_contra hf
  apply hd (m.le_degree (mem_support_iff.mpr hf))

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ (Fintype.card α).multichoose k = (Fintype.card α + k - 1).choose k

Tactic:
Nat.multichoose_eq

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ (Fintype.card α + k - 1).choose k = (Fintype.card α + k - 1).choose k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
· suffices m.degree g ≺[m] e by
      rw [m.coeff_eq_zero_of_lt this, mul_zero]
    simp only [not_lt] at hd
    apply lt_of_add_lt_add_left (a := m.toSyn d)
    grw [← map_add _ _ e, hd, ← map_add, hde]
    exact hc

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.zero
a : ℕ
h : DvdNotUnit (a + 1) 0
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if 0 = 0 then ⊤ else ↑0

pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if n✝ + 1 = 0 then ⊤ else ↑(n✝ + 1)

Tactic:
· simp

Goal state after:
case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if n✝ + 1 = 0 then ⊤ else ↑(n✝ + 1)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case h₁
σ : 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
⊢ (a, b) ∉ Finset.antidiagonal (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0

Tactic:
· simp

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

Goal state before:
pp: case inl
p : ℕ
hn : Squarefree 0
⊢ (factorization 0) p ≤ 1

pp: case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
· simp

Goal state after:
case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ n.factorization p ≤ 1
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
h0 : f * g ≠ 0
⊢ f ≠ 0

Tactic:
by grind

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
h0 : f * g ≠ 0
⊢ g ≠ 0

Tactic:
by grind

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
h0 : ¬f * g = 0
⊢ f ≠ 0

Tactic:
by grind

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
h0 : ¬f * g = 0
⊢ g ≠ 0

Tactic:
by grind

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 : f.support ⊆ g.support
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

Tactic:
by_cases hg : g = 0
  · simpa [hg] using h
  rw [m.withBotDegree_le_withBotDegree_iff_of_ne_zero _ hg]
  exact m.degree_le_degree_of_support_subset h

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)

pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = p.support.sup fun i ↦ ↑(i.sum fun x e ↦ e) / ↑(#S)

Tactic:
simp [← sum_div, Finsupp.sum_fintype]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ f.pmul ↑ζ = f

Tactic:
by
  ext x
  cases x <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ (↑ζ).pmul f = f

Tactic:
by
  ext x
  cases x <;> simp

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

Goal state before:
pp: case inl
n b : ℕ
hn : IsPrimePow n
hab : Coprime 0 b
⊢ n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b

pp: case inr
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
· simp

Goal state after:
case inr
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inl
n a : ℕ
hn : IsPrimePow n
ha : a ≠ 0
hab : a.Coprime 0
⊢ n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0

pp: case inr.inr
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b

Tactic:
· simp

Goal state after:
case inr.inr
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case inl
k : ℕ
⊢ (σ k) 0 = 0 ↔ 0 = 0

pp: case inr
k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
· simp

Goal state after:
case inr
k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = 0 ↔ n = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case inl
⊢ #(divisors 0) = 1 ↔ 0 = 1

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = 1 ↔ n = 1

Tactic:
· simp

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = 1 ↔ n = 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        (fun x ↦ (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }) (a x)) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
Function.Embedding.trans_apply,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        (fun x ↦ { toFun := PNat.val, inj' := PNat.coe_injective } (Additive.toMul.toEmbedding (a x))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a, Additive.ofMul.symm (∑ i, a i) = ⟨n, h⟩ ∧ (fun x ↦ ↑(Additive.toMul (a x))) = f) ↔ ∏ i, f i = n ∧ n ≠ 0

Tactic:
Additive.ofMul_symm_eq,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a, Additive.toMul (∑ i, a i) = ⟨n, h⟩ ∧ (fun x ↦ ↑(Additive.toMul (a x))) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
| succ n =>

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

Goal state before:
pp: N : ℕ
⊢ ∀ x ∈ Ioc 0 N, N / x = if x = 0 then 0 else N / x

Tactic:
by grind

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

Goal state before:
pp: case mpr
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 ℕ
hs : s.Finite
⊢ ∃ b, ∀ (i : ℕ), ∃ a, i ≤ a ∧ ¬b ≤ Nat.card ↑s • r

Tactic:
obtain ⟨m, hm⟩ := exists_lt_nsmul h (Nat.card s • r)

Goal state after:
case mpr
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 ℕ
hs : s.Finite
m : ℕ
hm : Nat.card ↑s • r < m • r
⊢ ∃ b, ∀ (i : ℕ), ∃ a, i ≤ a ∧ ¬b ≤ Nat.card ↑s • r
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ cutMap β ↑q
⊢ x ≤ ↑q

Tactic:
cutMap_coe

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
x : β
h : x ∈ Rat.cast '' {r | ↑r < ↑q}
⊢ x ≤ ↑q
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
cutMap_coe

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
q' : ℚ
hwq : w < ↑q'
hq : ↑q' < ↑q
⊢ ∃ a ∈ Rat.cast '' {r | ↑r < ↑q}, w < a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : 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))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = 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₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)

Tactic:
rw [← add_eq_zero_iff_neg_eq']

Goal state after:
σ : 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))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = 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₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ m.leadingCoeff (g b) + ∑ i ∈ B, m.leadingCoeff (g i) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → Coprime 0 n → f (0 * n) = f 0 * f n
hmn : Coprime 0 n
⊢ f (0 * n) = f 0 * f n

pp: case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
⊢ f (m * n) = f m * f n

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
⊢ f (m * n) = f m * f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → m.Coprime 0 → f (m * 0) = f m * f 0
hmn : m.Coprime 0
⊢ f (m * 0) = f m * f 0

pp: case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ f (m * n) = f m * f n

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ f (m * n) = f m * f n
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
f : ι → α
n : ℕ
hf : ∀ i ∈ ∅, 0 ≤ f i
⊢ (∑ i ∈ ∅, f i) ^ (n + 1) / ↑(#∅) ^ n ≤ ∑ i ∈ ∅, f i ^ (n + 1)

pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
f : ι → α
⊢ ((∑ i ∈ ∅, f i) / ↑(#∅)) ^ 2 ≤ (∑ i ∈ ∅, f i ^ 2) / ↑(#∅)

pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)

Tactic:
· simp

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑(#s)
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_1
ι : 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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hamax : toLex (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)) ≤ toLex (g a, f a)
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f ((Equiv.symm σ) a) ≤ f a

Tactic:
Prod.Lex.toLex_le_toLex

Goal state after:
case insert.inr.refine_1
ι : 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 α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
σ : Perm ι
hamax :
  (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 < (g a, f a).1 ∨
    (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).1 = (g a, f a).1 ∧
      (g ((Equiv.symm σ) a), f ((Equiv.symm σ) a)).2 ≤ (g a, f a).2
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f ((Equiv.symm σ) a) ≤ f a
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
rw [← Order.succ_eq_add_one, disjointed_succ _ hi]

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (succ i) = (partialSups f) i ⊔ f (succ i) \ (partialSups f) i