mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
⊢ 2 ≤ n →
    0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 →
      0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
⊢ 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1 → 0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (a_2 b : ℕ),
        a * (n / a) = n → a = a_2 → n / a = b → ∀ (a b_1 : ℕ), a' * (n / a') = n → a' = a → n / a' = b_1 → b_1 < b

Tactic:
rintro a b hab _ _ ha rfl rfl _ _ hb rfl rfl

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ n / b < n / a
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
⊢ 2 ≤ n →
    (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
      if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
⊢ (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
    if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 < 0 else 1 < x * ∑ i ∈ range n, x ^ i + 1

Tactic:
split_ifs at ihn ⊢ with hn'

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1

case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : ¬Even n
ihn : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
mul_ne_zero_iff

Goal state after:
case refine_2
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
obtain _ | _ | n := n

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 ≠ 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
hn : 0 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ 0 < ∑ i ∈ range (n + 1 + 1), x ^ i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
obtain _ | _ | n := n

Goal state after:
case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:

Tactic:
(a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

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

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
rintro rfl
    infer_instance

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

Goal state before:
pp: n a : ℕ
h : a < n
⊢ (↑a).val = a

Tactic:
rw [val_natCast, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).Coprime (n + (n + 1))

Tactic:
coprime_add_self_right,

Goal state after:
n : ℕ
⊢ (n + 1).Coprime n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ f.ker

Tactic:
rintro hf _ ⟨x, rfl⟩
          simp only [f.map_zsmul, zsmul_zero, f.mem_ker, hf]

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

Goal state before:
pp: m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
1,

Goal state after:
m k n : ℕ
| ∃ y, m * y + k = n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k n : ℕ
| ∃ y, m * y + k = n

Tactic:
1,

Goal state after:
m k n : ℕ
| fun y ↦ m * y + k = n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d % k + b' * ofDigits b' L % k) % k

Tactic:
Nat.mul_mod

Goal state after:
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
| (d % k + b' % k * (ofDigits b' L % k) % k) % k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head! = n.succ / (b + 2) ^ default % (b + 2)

Tactic:
head!_digits (by grind)

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ n.succ % (b + 2) = n.succ / (b + 2) ^ default % (b + 2)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdvd : a ∣ b
⊢ multiplicity a b ≠ 0

Tactic:
simpa [multiplicity_eq_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case convert_2
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = (fun x_1 ↦ x * x_1)^[minimalPeriod (fun x_1 ↦ x * x_1) 1] 1

Tactic:
rw [orderOf, mul_left_iterate_apply_one]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)

Tactic:
by
  refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
  · simpa using ((mem_fixedLengthDigits_iff hb).mp hL).1
  · intro x hx
    obtain rfl | hx := mem_cons.mp hx
    · exact hd
    · exact ((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p = 1

Tactic:
rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]

Goal state after:
case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
⊢ p ∈ Finset.range (n + 1) →
    p ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) p ((n.choose k).factorization p) = 1

Tactic:
_

Goal state after:
case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
⊢ p ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) p ((n.choose k).factorization p) = 1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ 1 ≤ i → i ≤ multiplicity m n → i < b

Tactic:
intro hi

Goal state after:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
⊢ i ≤ multiplicity m n → i < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ (↑(powers a)).Finite ↔ IsOfFinOrder a

Tactic:
refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
  obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])
  refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
  rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

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:
rw [← Nat.cast_pow, CharP.cast_eq_zero]

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

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
⊢ (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
_

Goal state after:
case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
⊢ (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
⊢ b ∈ f.support → b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0

Tactic:
_

Goal state after:
case pos.h₀
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ f.support
⊢ b ≠ n / p → (if p * b = n then f.coeff b else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
⊢ k ∈ f.support → (if p * k = n then f.coeff k else 0) = 0

Tactic:
_

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree

Tactic:
hq.degree_mul_comm,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.degree = (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) * q).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
⊢ (p %ₘ q).degree < q.degree

Tactic:
have :=
        degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
this : ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q).degree < q.degree
⊢ (p %ₘ q).degree < q.degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ n * 1 ≤ n * p

Tactic:
gcongr; exact hp.bot_lt

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p : R[X]
i : ℕ
⊢ i ∉ range (p.natDegree + 1) → (⇑derivative)^[i] p = 0

Tactic:
simp_all [iterate_derivative_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = ((X - C a) ^ if p = 0 then 0 else multiplicity (X - C a) p) * q ∧ ¬X - C a ∣ q

Tactic:
if_neg hp

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ multiplicity (X - C a) p * q ∧ ¬X - C a ∣ q
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ (FilterBasis.ofSets s).filter = generate s

Tactic:
by
  rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = C (eval 0 p)

Tactic:
rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ ((if p = 0 then 0 else multiplicity (X - C a) p) + 1) * q = p
⊢ False

Tactic:
if_neg hp

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ False
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i

Tactic:
classical
  simp only [mem_iInf, biInter_eq_iInter]
  refine ⟨?_, fun ⟨I, If, V, hVs, _, hVU, _⟩ => ⟨I, If, fun i => V i, fun i => hVs i, hVU⟩⟩
  rintro ⟨I, If, V, hV, rfl⟩
  refine ⟨I, If, fun i => if hi : i ∈ I then V ⟨i, hi⟩ else univ, fun i => ?_, fun i hi => ?_, ?_⟩
  · dsimp only
    split_ifs
    exacts [hV ⟨i,_⟩, univ_mem]
  · exact dif_neg hi
  · simp only [iInter_dite, biInter_eq_iInter, dif_pos (Subtype.coe_prop _), Subtype.coe_eta,
      iInter_univ, inter_univ, true_and]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

Tactic:
rw [le_rootMultiplicity_iff hzero]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ (X - C a) ^ min (rootMultiplicity a p) (rootMultiplicity a q) ∣ p + q
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n] (p * X) = (⇑derivative)^[n] p * X + n • (⇑derivative)^[n - 1] p

Tactic:
convert! p.iterate_derivative_mul_X_pow n 1; · simp
  rcases n with rfl | n <;> simp [sum_range_succ]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p * u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u

Tactic:
mul_ne_zero_iff

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
⊢ i ∈ univ → a i ∈ s i

Tactic:
_

Goal state after:
ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
a : (i : ι) → α i
ha : a ∈ {x | s x = univ}ᶜ.pi s
i : ι
a✝ : i ∈ univ
⊢ a i ∈ s i
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
nth_rw 1 [hr]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
nth_rw 1 [hr]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
q : M₀
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
⊢ (∀ x ∈ 0, Prime x) → (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
_

Goal state after:
case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
⊢ (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Multiset.Rel ?m.30 (normalizedFactors 1) 0

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Type ?u.21

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ α → ?m.29 → Prop

Tactic:
apply factors_unique irreducible_of_normalized_factor

Goal state after:
case inr.hg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ ∀ x ∈ 0, Irreducible x

case inr.h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ (normalizedFactors 1).prod ~ᵤ Multiset.prod 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
⊢ i ∈ Finset.range n → p.content ∣ p.coeff i

Tactic:
_

Goal state after:
case hab
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ p.content ∣ p.coeff i
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
⊢ i ∈ p.support → r ∣ p.coeff i

Tactic:
_

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
a✝ : i ∈ p.support
⊢ r ∣ p.coeff i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
a_unit : IsUnit a
⊢ a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
_

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
⊢ ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
⊢ p ∣ b → IsUnit p

Tactic:
_

Goal state after:
case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝² a : R
a_unit : IsUnit a
a✝¹ : a ≠ 0
b p : R
p_dvd_a : p ∣ a
a✝ : p ∣ b
⊢ IsUnit p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
x : ℕ
⊢ x ∈ Finset.range (max p.natDegree q.natDegree).succ → a ∣ p.coeff x - q.coeff x

Tactic:
_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
⊢ a ∣ p.coeff x - q.coeff x
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot
  clear hroot
  induction n with
  | zero =>
    simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _
  | succ n ih =>
    rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Goal state after: