mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ m.val.lists → x ≤ n.val.lists → x ≤ ⊥) ↔ ¬m = n

Tactic:
← m.coe_toList,

Goal state after:
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
⊢ (∀ ⦃x : Multiset (List α)⦄, x ≤ (↑m.toList).lists → x ≤ n.val.lists → x ≤ ⊥) ↔ ¬m = n
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
⊢ False

Tactic:
absurd h

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
a : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
⊢ m = n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
rw [permutationsAux_cons,
    length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
    permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),
    ← Nat.succ_eq_add_one, ← IH1, Nat.add_comm (_ * _), Nat.add_assoc, Nat.mul_succ, Nat.mul_comm]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'

Tactic:
intro xs' hxs' hd

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
hd : d ∈ xs'
⊢ xs.nextOr x d ∈ xs'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
dsimp only
        obtain ⟨n, hn⟩ := hab
        induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

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

Goal state before:
pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
rw [primeFactorsList] at h

Goal state after:
case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ n.primeFactorsList.length

Tactic:
by
  set k := n.primeFactorsList.length
  rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n | d ∣ n} = n.properDivisors

Tactic:
by
  ext
  simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
· simpa [ZMod.val_add] using! Nat.mod_le _ _

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
mul_inv_eq_gcd,

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑((↑x).val.gcd n) = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0

Tactic:
exact ⟨rfl, hn⟩

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(↑(u * u⁻¹)).val

Tactic:
rw [Units.val_mul, val_mul, natCast_mod]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b n : ℕ
⊢ b.digits n = [] ↔ n = 0

Tactic:
constructor
  · intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert! this
    rw [ofDigits_digits]
  · rintro rfl
    simp

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n b : ℕ
l : List ℕ
⊢ n * ofDigits b l = ofDigits b (List.map (fun x ↦ n * x) l)

Tactic:
by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

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

Goal state before:
pp: case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n

Tactic:
exact Nat.le_of_lt <| padicValNat_lt_self hn

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

Goal state before:
pp: case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ k

Tactic:
← pow_dvd_iff_le_of_spec hp hn h hl,

Goal state after:
case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p ^ (p.maxPowDvdDiv n).fst ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inr
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
simp [lt_one_iff.mp h]
    cases L
    · rfl
    · simp [ofDigits]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (bit b n).bits

Tactic:
| bit b n h ih =>

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b n : ℕ
h : b ≠ 1
⊢ (b.digits n).head! = n % b

Tactic:
by
  by_cases hb : 1 < b
  · rcases n with _ | n
    · simp
    · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
      rw [Nat.ofDigits_mod_eq_head! _ _]
      exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm
  · rcases n with _ | _ <;> simp_all [show b = 0 by lia]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : ↑k ≤ emultiplicity a b
⊢ a ^ k ∣ b

Tactic:
by classical
  cases k
  · simp
  unfold emultiplicity at hk
  split at hk
  · norm_cast at hk
    simpa using (Nat.find_min _ (lt_of_succ_le hk))
  · apply FiniteMultiplicity.not_iff_forall.mp ‹_›

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)

Tactic:
exact h.pow n

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(fixedLengthDigits hb l)

Tactic:
by
  rw [fixedLengthDigits, Set.coe_toFinset]
  convert! bijOn_digitsAppend hb l
  ext; simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
rw [add_assoc, tsub_add_cancel_of_le (succ_le_of_lt hm0)]
              simp_all [mul_comm, mul_left_comm, pow_add]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
⊢ x ^ a = x ^ b

Tactic:
by
  obtain hle | hle := le_total a b
  all_goals
    obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle
    obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h
    simp [pow_add, pow_mul, hx]

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

Goal state before:
pp: case zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ 0 ^ a.factorization 0 ∣ 0 ^ b.factorization 0 ↔ a.factorization 0 ≤ b.factorization 0

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

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

Goal state before:
pp: case succ.zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (0 + 1) ^ a.factorization (0 + 1) ∣ (0 + 1) ^ b.factorization (0 + 1) ↔
    a.factorization (0 + 1) ≤ b.factorization (0 + 1)

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

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

Goal state before:
pp: case succ.succ
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (p + 1 + 1) ^ a.factorization (p + 1 + 1) ∣ (p + 1 + 1) ^ b.factorization (p + 1 + 1) ↔
    a.factorization (p + 1 + 1) ≤ b.factorization (p + 1 + 1)

Tactic:
simp [Nat.pow_dvd_pow_iff_le_right]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
⊢ emultiplicity p (a ^ 0) = ↑0 * emultiplicity p a

Tactic:
simp [emultiplicity_of_one_right hp.not_isUnit]

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

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = n.factorization q

Tactic:
factorization_div (ordProj_dvd n p)

Goal state after:
case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Goal state after:
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p

case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
⊢ a ∣ b

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Goal state after:
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
· rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n ≡ m [ZMOD ↑0]
⊢ n = m

Tactic:
Nat.cast_zero,

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : n ≡ m [ZMOD 0]
⊢ n = m
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 ≤ p.divX.degree

Tactic:
rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ ↑p ^ i = 0

Tactic:
← Nat.cast_pow,

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ ↑(p ^ i) = 0
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a b : R
f g : R[X]
hf : f.coeff n = a
hg : g.coeff n = b
⊢ (f - g).coeff n = a - b

Tactic:
subst hf hg; apply coeff_sub

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX

Tactic:
← add_zero (X * f.divX),

Goal state after:
R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX + 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p = 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).degree = ↑(f.natDegree * p)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

Tactic:
Nat.cast_zero,

Goal state after:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (p.coeff 0 * 0 * if n = 0 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 /ₘ p = 0

Tactic:
grind [divByMonic, divModByMonicAux]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n), f.coeff x.1 * ((expand R p) g).coeff x.2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
sum_image

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Set.InjOn (fun x ↦ (x.1 * p, x.2 * p)) ↑(antidiagonal n)

case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ f.coeff (p * x, p * y).1 * ((expand R p) g).coeff (p * x, p * y).2 = 0

Tactic:
refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = n * p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p) ((monomial n) a)) = (monomial n) a ^ p

Tactic:
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
      mul_pow, ← C.map_pow, frobenius_def]
    ring

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1))

Tactic:
sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (∑ a ∈ range (n + 1), C (p.coeff a * ↑a) * X ^ (a - 1))

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
r a : R
⊢ rootMultiplicity a (C r) = 0

Tactic:
by
  cases subsingleton_or_nontrivial R
  · rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
  classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (univ.pi s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
constructor
  · simp only [inf_principal_eq_bot, mem_pi]
    contrapose!
    rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
    have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
    choose x hxs hxt using this
    exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
  · simp only [inf_principal_eq_bot]
    rintro ⟨i, hi⟩
    filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
by
  simp only [neBot_iff, Ne, prod_eq_bot, not_or]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
P : R[X]
h : P.degree < ↑k
⊢ (⇑derivative)^[k] P = 0

Tactic:
induction k generalizing P
  case zero => exact degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h
  case succ k ind =>
    by_cases P = 0
    case pos hP => simp [hP]
    case neg hP =>
      rw [Function.iterate_add_apply, Function.iterate_one]
      by_cases derivative P = 0
      case pos hP' => simp [hP']
      case neg hP' =>
        have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
        refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
        linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case insert
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
classical
    convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
unfold roots

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(if h : p = 0 then ∅ else Classical.choose ⋯).card ≤ p.degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
normalizedFactors,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (factors a)).prod ~ᵤ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod

Tactic:
normalizedFactors,

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (factors a)).prod = normalize (Multiset.map normalize (factors a)).prod