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

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

Tactic:
← not_le,

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ ¬Odd n → ¬x + 1 ≤ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)

Tactic:
rw [Ico_eq_empty_of_le (by lia), sum_empty]

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Tactic:
rintro rfl
    simp

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

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) +
          (∑ x ∈ Ico 1 tl.length, ofDigits p (List.drop x tl) +
            ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ i ∈ Ico 1 (tl.length + 1), ofDigits p (List.drop i tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h_2 : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h_2)

Tactic:
simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (fixedLengthDigits hb l).card = b ^ l

Tactic:
by
  rw [Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l), Finset.card_range]

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

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f

Tactic:
sum_congr rfl (hf · · |>.factorization_pow)

Goal state after:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ ∑ x1 ∈ f.support, single x1 (f x1) = f
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: k p : ℕ
hp : Prime p
m : ℕ
⊢ m / p ^ m.factorization p = p ^ k * m / p ^ (p ^ k * m).factorization p

Tactic:
← ordCompl_self_pow_mul m k hp

Goal state after:
k p : ℕ
hp : Prime p
m : ℕ
⊢ p ^ k * m / p ^ (p ^ k * m).factorization p = p ^ k * m / p ^ (p ^ k * m).factorization p
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p * p)

Tactic:
Nat.div_mul_cancel (hp.dvd_choose_pow _ _)

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) = x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k)

R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
intro e hea heb

Goal state after:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow p]
  rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]

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

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
⊢ emultiplicity p (p * p ^ n)! = ↑(∑ i ∈ range (n + 1), p ^ i)

Tactic:
hp.emultiplicity_factorial_mul,

Goal state after:
case succ
p : ℕ
hp : Prime p
n : ℕ
h : emultiplicity p (p ^ n)! = ↑(∑ i ∈ range n, p ^ i)
⊢ emultiplicity p (p ^ n)! + ↑(p ^ n) = ↑(∑ i ∈ range (n + 1), p ^ i)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ ↑r ≤ ↑(∑ i ∈ Ico 1 b, n / p ^ i)

Tactic:
← hp.emultiplicity_factorial hbn,

Goal state after:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ ↑r ≤ emultiplicity p n !
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ x = y ∨ x⁻¹ = y → zpowers x = zpowers y

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x

case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers x⁻¹
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)

Tactic:
rw [← hp.emultiplicity_mul]

Goal state after:
p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1) * (k + 1))
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
rintro rfl
    simp

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

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)

Tactic:
let m' := m / gcd m n

Goal state after:
a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
⊢ ∃ c, a = c ^ (n / g) ∧ b = c ^ (m / g)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inr.inr
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)
p q : R[X]
hp : M p
hq : M q
⊢ (p + q).natDegree = 0 ∨ M (p + q)

Tactic:
exact Or.inr (h_add hp hq)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
r : R
⊢ (expand R p) ((expand R q) (C r)) = (expand R (p * q)) (C r)

Tactic:
simp_rw [expand_C]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun a b ↦ ((monomial (p * a)) b).coeff n) = if p ∣ n then f.coeff (n / p) else 0

Tactic:
coeff_monomial,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (f.sum fun a b ↦ if p * a = n then b else 0) = if p ∣ n then f.coeff (n / p) else 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic 0
⊢ p /ₘ 0 = 0

Tactic:
by unfold divByMonic divModByMonicAux; rw [dif_neg h]

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 : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
⊢ (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y → x = y

Tactic:
eq

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
eq : (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y
⊢ x = y
Module: Mathlib.Algebra.Polynomial.Expand

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

Tactic:
eq

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
⊢ (derivative p).degree = p.degree

Tactic:
rw [H, derivative_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
        exact Nat.le_add_right _ _

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).1
      else 0).degree ≤
    p.degree

Tactic:
simp [dif_pos hq, h, degree_zero, bot_le]

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

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

Tactic:
rw [rootMultiplicity_eq_multiplicity]

Goal state after:
case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ (if C r = 0 then 0 else multiplicity (X - C a) (C r)) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ X ^ n = ↑(n.descFactorial 0) * X ^ n

Tactic:
Nat.descFactorial_zero,

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ X ^ n = ↑1 * X ^ n
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ x, s ↑x ⊆ t
i : ↑I
⊢ s ↑i ∈ ⨅ (_ : p ↑i), 𝓟 (s ↑i)

Tactic:
simp [hpI i i.2]

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

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

Tactic:
by
  convert! (derivative^[2] p).iterate_derivative_mul_X_pow n 2
  rcases n with rfl | n; · simp
  rcases n with rfl | n; · simp [sum_range_succ, ← mul_assoc]
  suffices ((n + 1 + 1) * (n + 1) / 2) * 2 = (n + 1 + 1) * (n + 1) by
    simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
    ring
  rw [mul_comm (n + 1 + 1)]
  exact Nat.div_mul_cancel (Nat.two_dvd_mul_add_one _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : f₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
have := neBot_of_le hle.2

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

Tactic:
refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
  rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
  exact fun x _ => h x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

Tactic:
by
  simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
  rfl

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s : Multiset ι
f : ι → M₀
h : p ∣ (Multiset.map f s).prod
⊢ ∃ a ∈ s, p ∣ f a

Tactic:
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
    hp.exists_mem_multiset_dvd h

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

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
x : R
hx : ((fun x ↦ eval x p) ⁻¹' {x}).Infinite
⊢ False

Tactic:
obtain ⟨rfl⟩ : p = C x := p.eq_of_infinite_eval_eq (C x) (by simpa)

Goal state after:
R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hp : (C x).natDegree ≠ 0
hx : ((fun x_1 ↦ eval x_1 (C x)) ⁻¹' {x}).Infinite
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ count s (X - C r).roots = count s {r}

Tactic:
rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
· simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ normalizedFactors (x ^ n) = n • normalizedFactors x

Tactic:
induction n with
  | zero => simp [zero_nsmul]
  | succ n ih =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
· simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
⊢ (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
    map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
eq

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Goal state after:
case inl
α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
x : α
⊢ x ∈ normalizedFactors 0 ↔ ↑f x ∈ normalizedFactors (f 0)

case inr
α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
ha : a ≠ 0
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * p.primPart

Tactic:
primPart,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * if p = 0 then 1 else Classical.choose ⋯
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)

Tactic:
apply dvd_sub (Dvd.intro _ rfl) (Dvd.intro _ rfl)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ (Associates.mk a).factors.prod = Associates.mk a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (Associates.mk 0).factors.prod = Associates.mk 0

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ (Associates.mk a).factors.prod = Associates.mk a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
a✝ : Nontrivial α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
exact ⟨fun h ↦ by rwa [← factors_prod a, FactorSet.prod_eq_zero_iff], fun h ↦ h ▸ factors_zero⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod ↑(factors' a0)

Tactic:
rw [prod_coe]

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ (Multiset.map Subtype.val (factors' a0)).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors = 0 ∨ p.count b.factors = 0

Tactic:
by
  rw [or_iff_not_imp_left, ← Ne]
  intro hca
  contrapose! hab with hcb
  exact ⟨p, le_of_count_ne_zero ha hp hca, le_of_count_ne_zero hb hp hcb,
    UniqueFactorizationMonoid.irreducible_iff_prime.mp hp⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
z : DirectLimit F f
x y : (i : ι) × F i
x✝ : x ≈ y
k : ι
hxk : x.fst ≤ k
hyk : y.fst ≤ k
eq : (f x.fst k hxk) x.snd = (f y.fst k hyk) y.snd
⊢ ih k ((f x.fst k hxk) x.snd) = ih k ((f y.fst k hyk) y.snd)

Tactic:
eq

Goal state after: