mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ p.divX ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ ¬p = C (p.coeff 0)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ |x| ^ n = 1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ |x| ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Tactic:
simpa using

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
b : β
⊢ 0 < orderOf a → 0 < orderOf b → 0 < (orderOf a).lcm (orderOf b)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ m * a.factorization p = n * b.factorization p

Tactic:
simpa using

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ m * a.factorization p = n * b.factorization p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ r.natDegree = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ r.natDegree = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this✝ : Invertible a := ha.invertible
this :
  rootMultiplicity (a * c + b) ((p.comp (C a * X + C b)).comp (C ⅟a * X + C (-⅟a * b))) ≤
    rootMultiplicity (⅟a * (a * c + b) + -⅟a * b) (p.comp (C a * X + C b))
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this✝ : Invertible a := ha.invertible
this :
  rootMultiplicity (a * c + b) ((p.comp (C a * X + C b)).comp (C ⅟a * X + C (-⅟a * b))) ≤
    rootMultiplicity (⅟a * (a * c + b) + -⅟a * b) (p.comp (C a * X + C b))
⊢ rootMultiplicity (a * c + b) p ≤ rootMultiplicity c (p.comp (C a * X + C b))
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).Monic

Tactic:
by
  simp only [Monic]
  calc
    ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

Goal state after:
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
⊢ f.natDegree + 1 ≤ n * 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree + 1 ≤ n
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = X - C (-p.coeff 0)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = X + C (p.coeff 0)
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)
eq : (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y
⊢ x = y

Tactic:
simpa using

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.1 = y.1 ∧ x.2 = y.2
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime ((C a * X + C b).coeff 0) ((C a * X + C b).coeff 1)

Tactic:
simpa using

Goal state after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
ha : a ≠ 0
hab : IsRelPrime a b
⊢ IsRelPrime b a
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ q ∣ p %ₘ q ↔ q ∣ p

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
⊢ q ∣ p %ₘ q ↔ q ∣ p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
⊢ (X - C x).degree ≤ p.degree

Tactic:
simpa using

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
⊢ 1 ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = g.natDegree + (f /ₘ g).natDegree - g.natDegree

Tactic:
add_tsub_cancel_left

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = (f /ₘ g).natDegree
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
⊢ r - f %ₘ g = 0

Tactic:
simpa using

Goal state after:
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
⊢ r - f %ₘ g = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q) +
      n.choose n.succ • ((⇑derivative)^[n - n] p * (⇑derivative)^[n + 1] q)

Tactic:
Nat.choose_succ_self,

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q) +
      0 • ((⇑derivative)^[n - n] p * (⇑derivative)^[n + 1] q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp 1 = Finsupp.single 0 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp 1 = Finsupp.single 0 1
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
eq_C_of_degree_le_zero this,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (C ((p %ₘ (X - C a)).coeff 0)) = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
eq_C_of_degree_le_zero this,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ C ((p %ₘ (X - C a)).coeff 0) = C (eval a p)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
this : X - C b ∣ p - C (eval b p)
⊢ a - b ∣ eval a p - eval b p

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
this : X - C b ∣ p - C (eval b p)
⊢ a - b ∣ eval a p - eval b p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
h : p.IsRoot x
⊢ x ∣ p.coeff 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
h : p.IsRoot x
⊢ x ∣ eval 0 p
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
this : update g i x ∈ I'.pi t
⊢ x ∈ s i

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
this : update g i x ∈ I'.pi t
⊢ x ∈ s i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ⋂ i ∈ I ∩ {i | p i}, s i ⊆ ⋂ i, V i

Tactic:
simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_ofPred_eq]

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ⋂ x, ⋂ (_ : p ↑x), s ↑x ⊆ ⋂ i, ⋂ (i_1 : p ↑i), t i i_1
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ Pairwise fun i j ↦ ∃ s t, Disjoint ↑s ↑t

Tactic:
simpa using

Goal state after:
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∀ ⦃i j : ι⦄, i ≠ j → ∃ a ∈ l i, ∃ a_1 ∈ l j, Disjoint a a_1
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a ↦ if h : a ∈ s then p ⟨a, h⟩ else univ) a ∈ f a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ p ⟨a, ⋯⟩ ∈ f a
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: 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 : k ≤ m
⊢ n < k

Tactic:
simpa using

Goal state after:
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 : k ≤ m
⊢ n < k
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree ≤ p.degree
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i.down) = 𝓟 (⋂ i, f i.down)

Tactic:
simpa using

Goal state after:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i.down) = 𝓟 (⋂ i, f i.down)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x

Tactic:
simpa using

Goal state after:
α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ ⋂ i, {x | p i x} ∈ l ↔ ∀ (i : ι), {x | p i x} ∈ l
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ pi f = ⊥ ↔ ∃ i, f i = ⊥
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x

Tactic:
simpa using

Goal state after:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ ⋂ i ∈ I, {x | p i x} ∈ l ↔ ∀ i ∈ I, {x | p i x} ∈ l
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
f : Filter ι
s : ι → Set α
t : Set α
ht : t.Finite
hs : ∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i
⊢ ∀ᶠ (i : ι) in f, t ⊆ s i

Tactic:
simpa using

Goal state after:
α : Type u
ι : Type u_2
f : Filter ι
s : ι → Set α
t : Set α
ht : t.Finite
hs : ∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i
⊢ ∀ i ∈ t, ∀ᶠ (x : ι) in f, i ∈ s x
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ f = ⊥

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Filter.coprodᵢ f = ⊥ ↔ ∀ (x : ι), f x = ⊥
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hpq : p ∣ 0
h₁ : natDegree 0 ≤ p.natDegree
h₂ : p.leadingCoeff = leadingCoeff 0
⊢ p = 0

Tactic:
simpa using

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hpq : p ∣ 0
h₁ : natDegree 0 ≤ p.natDegree
h₂ : p.leadingCoeff = leadingCoeff 0
⊢ p = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ q.natDegree ≤ (p * ↑((Units.map ↑C) u)).natDegree

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ q.natDegree ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ (p * ↑((Units.map ↑C) u)).leadingCoeff = q.leadingCoeff

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ p.leadingCoeff * ↑u = q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff

Tactic:
rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
h₁ : p.degree = q.degree
hq : q = 0
⊢ p = q

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
h₁ : p.degree = q.degree
hq : q = 0
⊢ p = 0
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hi : i ∈ I
⊢ f i ⁻¹' f i '' s i ∈ l i
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Finite
⊢ cofinite ⊓ 𝓟 sᶜ = cofinite

Tactic:
simpa using

Goal state after:
α : Type u_2
s : Set α
hs : s.Finite
⊢ s.Finite
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
x : α
x✝ : ∃ i, ∃ (_ : i ∈ f), x ∉ i
s : Set α
hs : s ∈ f
hx : x ∉ s
⊢ s ⊆ {x}ᶜ

Tactic:
simpa using

Goal state after:
α : Type u_2
f : Filter α
x : α
x✝ : ∃ i, ∃ (_ : i ∈ f), x ∉ i
s : Set α
hs : s ∈ f
hx : x ∉ s
⊢ x ∉ s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case h
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x ↦ b) id (a, i') = (b', i')

Tactic:
simpa using

Goal state after:
case h
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ b = b'
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = (𝓟 q.1 ⊔ q.2).ker
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
rw [ker_sup, ker_principal, le_cofinite_iff_ker.mp hq.1, union_empty] at hqk

Goal state after:
case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q = (f.ker, Coheyting.boundary f)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.map (fun a ↦ X - C a) (S.erase r)).prod =
    (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a ↦ X - C a) (S.erase r))).prod
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.map (fun a ↦ X - C a) (S.erase r)).prod =
    (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a ↦ X - C a) (S.erase r))).prod
⊢ eval r (Multiset.map (fun a ↦ X - C a) (S.erase r)).prod = (Multiset.map (fun a ↦ r - a) (S.erase r)).prod
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ (f ⁻¹' s).Finite

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ (f ⁻¹' s).Finite
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ (f ⁻¹' {b}).Finite

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ (f ⁻¹' {b}).Finite
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ y.support ⊆ s

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ ∀ ⦃x : α⦄, ¬y x = 0 → ∃ x_1, ¬y x_1 = 0 ∧ f x_1 = f x ∧ ¬y x_1 = 0
Module: Mathlib.Algebra.BigOperators.Associated

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

Tactic:
simpa using

Goal state after:
M₀ : Type u_3
inst✝ : CommMonoidWithZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : p ∣ s.prod → ∃ a ∈ s, p ∣ a
h : p ∣ (a ::ₘ s).prod
⊢ p ∣ a * s.prod
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 using

Goal state after:
ι : 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
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y

Tactic:
exact hprod

Goal state after: