mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : ∑ i ∈ (n✝ + 1).properDivisors \ s, 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Tactic:
simp only [sum_const_zero] at hlt

Goal state after:
case bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Tactic:
exact n.descFactorial_le_pow r

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

Goal state before:
pp: case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ (n + 1 + 1).choose 0 ≤ 2 ^ (n + 1)

Tactic:
rw [choose_zero_right]
        exact Nat.one_le_two_pow

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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n

Tactic:
rw [mul_assoc, mul_comm (2 * n + 1)]

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (l ++ [0]) = ofDigits b l

Tactic:
by
  rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]

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

Goal state before:
pp: case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ (d :: L).getLast ⋯ = 0

Tactic:
refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_

Goal state after:
case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ (d :: L).getLast ⋯ ∈ L
Module: Mathlib.Data.Nat.MaxPowDiv

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

Tactic:
← pow_padicValNat_mul_divMaxPow p n,

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n

Tactic:
refine Nat.succ_le_of_lt (log_pos hb ?_)

Goal state after:
case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ b ≤ n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
this : L = l
⊢ D :: L = d :: l

Tactic:
rw [eqd, this]

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

Goal state before:
pp: case succ
p n : ℕ
a✝ : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1

Tactic:
induction p with

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ ↑(multiplicity a b) ≤ ↑n

Tactic:
assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b

Tactic:
assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ ↑(multiplicity a b) < ↑n

Tactic:
assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b

Tactic:
assumption_mod_cast

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝ : ℕ
h : x✝ ∈ {n | n < b ^ l}
⊢ (b.digitsAppend l x✝).length = l

Tactic:
by rw [length_digitsAppend hb _ h]

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

Goal state before:
pp: case refine_2
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
x✝ : d ∣ d * c
⊢ d.factorization ≤ d.factorization + c.factorization

Tactic:
apply self_le_add_right

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 ∣ a
x : α
hx : a = p * x
hn0 : n = 0
⊢ False

Tactic:
simp [hx, hn0] at ha

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

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ (p ^ k).factorization ≤ n.factorization ↔ k ≤ n.factorization p

Tactic:
pp.factorization_pow,

Goal state after:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ single p k ≤ n.factorization ↔ k ≤ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

Tactic:
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]

Goal state after:
case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ ¬False ∨ n / q ^ n.factorization q = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: 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
⊢ orderOf (x * y) = orderOf y

Tactic:
have hoy := hy.orderOf_pos
  have hxy := dvd_of_forall_prime_mul_dvd hdvd
  apply orderOf_eq_of_pow_and_pow_div_prime hoy <;> simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
  · exact h.orderOf_mul_dvd_lcm.trans (Nat.lcm_dvd hxy dvd_rfl)
  refine fun p hp hpy hd => hp.ne_one ?_
  rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]
  refine (orderOf_dvd_lcm_mul h).trans (Nat.lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)
  by_cases h : p ∣ orderOf x
  exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]

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

Goal state before:
pp: case pos
p n k : ℕ
h : (n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
· simp [h]

Goal state after:
case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
rw [two_mul, add_tsub_cancel_left]

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

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
⊢ p ∈ (n.choose k).factorization.support → p ∈ Finset.range (n + 1)

Tactic:
hp

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p ∈ Finset.range (n + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ i < b

Tactic:
rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]

Goal state after:
case succ
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ (p + 1) ^ i < (p + 1) ^ b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
simpa [emultiplicity_mul, h2, prime_two, bit, factorial]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ g ^ H.index ∈ H

Tactic:
rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

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

Goal state before:
pp: case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
⊢ p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support → p ^ padicValNat p n = 1

Tactic:
hp

Goal state after:
case hg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
⊢ p ^ padicValNat p n = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
⊢ p ∈ n.factorization.support → (fun x1 x2 ↦ x1 ^ x2) p (n.factorization p) = p ^ padicValNat p n

Tactic:
hp

Goal state after:
case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ n.factorization.support
⊢ (fun x1 x2 ↦ x1 ^ x2) p (n.factorization p) = p ^ padicValNat p n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
p1 p2 : ↥n.primeFactors
⊢ p1 ≠ p2 → Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 p2

Tactic:
hp

Goal state after:
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Function.onFun Coprime (fun p ↦ ↑p ^ n.factorization ↑p) p1 p2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
pow_mem : ∀ a ∈ S, ∀ (n : ℕ), a ^ (n + 1) ∈ S
⊢ 1 ∈ S

Tactic:
obtain ⟨a, ha⟩ := hS1
      rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
      exact pow_mem a ha (orderOf a - 1)

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : ℤ
⊢ (↑a).coeff n = ↑(if n = 0 then a else 0)

Tactic:
simp only [← C_eq_intCast, coeff_C, Int.cast_ite, Int.cast_zero]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ p.natDegree - 0

Tactic:
Nat.sub_zero

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n + 1 = 0
⊢ 0 = f.coeff (n + 1)

Tactic:
← Nat.cast_succ,

Goal state after:
case neg.succ.inr
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : ↑n.succ = 0
⊢ 0 = f.coeff (n + 1)
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:
expand_monomial,

Goal state after:
case refine_2
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((monomial (n * p)) a) = (monomial n) a ^ p
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ Algebra.IsAlgebraic R ↥S

Tactic:
Algebra.isAlgebraic_def

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), IsAlgebraic R x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 ≤ i - (n + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ C (↑n + 1) * p ^ n * derivative p * p + p ^ (n + 1) * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
Nat.add_one,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ C (↑n + 1) * p ^ n * derivative p * p + p ^ n.succ * derivative p = C (↑n.succ + 1) * p ^ n.succ * derivative p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, ¬¬(X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Tactic:
not_not

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, (X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : (X - C x).degree = 0
⊢ p.degree = 1

Tactic:
h₁

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ p.degree = 1
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr✝ : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
a✝ : α
⊢ p a✝ → q (y a✝) → r a✝ (y a✝)

Tactic:
hp

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr✝ : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
a✝ : α
hp : p a✝
⊢ q (y a✝) → r a✝ (y a✝)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc
h₂ : Tendsto f (la ×ˢ ⊤) lc
⊢ Tendsto f (la.coprod lb) lc

Tactic:
by
  simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
la : Filter α
lb : Filter β
lc : Filter γ
h₁ : ∀ s ∈ lb, Tendsto f (la ×ˢ 𝓟 sᶜ) lc
h₂ : Tendsto f (⊤ ×ˢ lb) lc
⊢ Tendsto f (la.coprod lb) lc

Tactic:
by
  simp_all [tendsto_prod_iff, coprod_eq_prod_top_sup_top_prod]
  grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ (factors a).card = (factors b).card

Tactic:
by_cases hb : b = 0
  · simp_all
  have ha : a ≠ 0 := h.ne_zero_iff.mpr hb
  apply Multiset.card_eq_card_of_rel
  apply factors_unique irreducible_of_factor irreducible_of_factor
  exact (factors_prod ha).trans <| h.trans (factors_prod hb).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯)).prod ~ᵤ a

Tactic:
dif_neg ane0

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (Classical.choose ⋯)).prod ~ᵤ a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a p.roots = rootMultiplicity a p

Tactic:
rw [roots_def, dif_neg hp]

Goal state after:
case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose ⋯) = rootMultiplicity a p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ normalizedFactors a

Tactic:
hp

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
⊢ p ∈ normalizedFactors a → ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
hp

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
⊢ ∀ q ∈ normalizedFactors a, p ∣ q → p = q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X + C b).roots = {-(↑a⁻¹ * b)}

Tactic:
by
  rw [← sub_neg_eq_add, ← C_neg, roots_C_mul_X_sub_C_of_IsUnit, mul_neg]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0

Tactic:
by_contra hp

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ Fintype R

Tactic:
exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
dif_neg ane0

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
rw [dif_neg ane0]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
⊢ Irreducible p ↔ Prime p

Tactic:
by_cases hp0 : p = 0
  · simp [hp0]
  refine ⟨fun h => ?_, Prime.irreducible⟩
  obtain ⟨f, hf⟩ := pf p hp0
  obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf
  rw [hq.prime_iff]
  exact hf.1 q (Multiset.mem_singleton_self _)

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
hp : p.Monic
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ (aeval a) p = 0

Tactic:
by
  simp [Polynomial.mem_rootSet', (hp.map (algebraMap T S)).ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

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

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:
· simp [h]

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 * p.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p.primPart.IsPrimitive