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

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : Finite σ
this : Fintype σ
⊢ ∀ (α : Type u_1) [Fintype α],
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
intro α _ H P
    obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
    simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q

Tactic:
exact mul_dvd_mul_left (X i) hq

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

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 1 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
Fintype.sum_subsingleton

Goal state after:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 1 = ↑(↑↑?empty.zero.a).countPerms * (Multiset.map x ↑↑?empty.zero.a).noncommProd ⋯

case empty.zero.a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ ↥(∅.sym 0)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
· rw [_root_.pow_succ, mul_zero]
      have : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
      apply (Fintype.sum_empty _).symm

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ x₁ j = x j

Tactic:
try rfl

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ x₁ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ x j = x j

Tactic:
try rfl

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j

Tactic:
try rfl

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ x₁ j = x j

Tactic:
try rfl

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ x₁ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j

Tactic:
try rfl

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ x j = x j

Tactic:
try rfl

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
hbc : degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) < toLex (ofDegLex c)
⊢ degree (ofDegLex a) < degree (ofDegLex c) ∨
    degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

Tactic:
· right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
p : Fin (n + 1)
⊢ f ∈ piFinset s ↔ f p ∈ s p ∧ p.removeNth f ∈ piFinset (p.removeNth s)

Tactic:
simp only [Fintype.mem_piFinset, forall_iff_succAbove p, removeNth]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last (last n) ∈ snoc s_init s_last (last n) ∧
      init (snoc x_init x_last) ∈ piFinset (init (snoc s_init s_last)) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset s_init

Tactic:
init_snoc,

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last (last n) ∈ snoc s_init s_last (last n) ∧ x_init ∈ piFinset s_init ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset s_init
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h₁
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 ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) ≤
    pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))

Tactic:
calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
            ≤ #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0) := by
            gcongr with x; exact And.right
          _ = #(S 0) * #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0}
              / (#(S 0) * (∏ i, #(S (.succ i)) : ℚ≥0)) := by
            rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]
            norm_cast
          _ ≤ #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0} / ∏ i, (#(S (.succ i)) : ℚ≥0) :=
            mul_div_mul_left_le (by positivity)
          _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S (.succ i)) : ℚ≥0)) :=
            schwartz_zippel_sup_sum hpₖ₀ _

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 : MvPolynomial σ R
a : σ →₀ ℕ
ha : a ∈ p.support
⊢ m.toSyn a ≤ m.toSyn (m.degree p)

Tactic:
by
  simp [degree, Finset.le_sup ha]

Goal state after:
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 k ∣ n then if k ∣ n / k then some k else (n / k).minSqFacAux (k + 2) else n.minSqFacAux (k + 2))

Tactic:
have k2 : 2 ≤ k := by lia

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
k2 : 2 ≤ 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: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

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
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

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
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)
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) R
hp : p ≠ 0
S : Finset R
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
obtain rfl | hs := S.eq_empty_or_nonempty

Goal state after:
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 / ↑(#∅)

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:
rw [sup_div₀ (by positivity)]

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.support.sup fun i ↦ ↑(i.sum fun x e ↦ e) / ↑(#S)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, f x.2 * ↑(ζ x.1) = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * ↑(ζ x.2)

Tactic:
rw [sum_divisorsAntidiagonal fun x y ↦ f y * ζ x, sum_divisorsAntidiagonal' fun x y ↦ f x * ζ y]

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

Goal state before:
pp: case e'_4
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 = b ^ 2 * x ^ 2

Tactic:
rw [mul_pow]

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

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
h0 : f = 0 ∨ g = 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
(obtain rfl | rfl := h0) <;> simp

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

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactorsList.toFinset, p = n

Tactic:
List.prod_toFinset _ hn.nodup_primeFactorsList,

Goal state after:
n : ℕ
hn : Squarefree n
⊢ (List.map (fun p ↦ p) n.primeFactorsList).prod = n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inl
b : ℕ
hab : Coprime 0 b
⊢ {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}

Tactic:
simp only [Nat.coprime_zero_left] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]

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

Goal state before:
pp: case mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0

Tactic:
rintro ⟨f, hf, rfl⟩
    exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap β γ (inducedMap α β a) ↔ ↑q < inducedMap α γ a

Tactic:
by
    rw [coe_lt_inducedMap_iff, coe_lt_inducedMap_iff, Iff.comm, coe_lt_inducedMap_iff]

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
⊢ ∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i

Tactic:
convert!
    hfg.sum_smul_comp_perm_le_sum_smul
      (show {x | σ⁻¹ x ≠ x} ⊆ s by simp [set_support_symm_eq, hσ]) using 1

Goal state after:
ι : 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
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
exact ha

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

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
exact ha

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

Goal state before:
pp: case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := ⋯
⊢ #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r \ s, x

Tactic:
refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
x : ℤ
mx : x ∈ r \ s
⊢ c - ↑(#s) ≤ x
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 * (↑x).2

Tactic:
by
          rw [← h]
          exact x.2.2.2.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s t : Set α
a : α
x y : ↑(s.mulAntidiagonal t a)
h : (↑x).2 = (↑y).2
⊢ a = (↑x).1 * (↑y).2

Tactic:
by
          rw [← h]
          exact x.2.2.2.symm

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n))
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun x1 x2 ↦ x1 ≤ x2) (fun x ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (?m.120 m))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h) (?m.120 n))
⊢ (Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g m) = (Infinite.natEmbedding (s.mulAntidiagonal t a) h) (g n)

Tactic:
exact eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'

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

Goal state before:
pp: case neg.coe.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
a✝ : NonemptyInterval α
ha : ↑a✝ ∈ x✝
⊢ ↑a✝ ∈ x✝

Tactic:
exact ha

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

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

Tactic:
rw [h, leadingCoeff_zero, coeff_zero]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b✝ : Γ
r : R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∈ Function.support fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0
⊢ b ∈ ⇑f '' x.support

Tactic:
contrapose hb

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b✝ : Γ
r : R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ ⇑f '' x.support
⊢ b ∉ Function.support fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ (embDomain f x).coeff (f a) = x.coeff a

Tactic:
rw [embDomain]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
⊢ { coeff := fun b ↦ if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }.coeff
      (f a) =
    x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ ((truncLT c) x).support = {y | y ∈ x.support ∧ y < c}

Tactic:
simp [truncLT, Function.support, and_comm]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).orderTop = x.orderTop

Tactic:
by
  rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact orderTop_add_eq_left hxy

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
a : Γ
r : R
s : V
b : Γ
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b

Tactic:
by_cases h : b = a

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
a : Γ
r : R
s : V
b : Γ
h : b = a
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
a : Γ
r : R
s : V
b : Γ
h : ¬b = a
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (ofLex ((n + 1) • |x|)).coeff j_1
hi : (ofLex |y|).coeff j < (ofLex ((n + 1) • |x|)).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
ofLex_smul,

Goal state after:
case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = ((n + 1) • ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < ((n + 1) • ofLex |x|).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|