mathlib-initiative/mathlib-tactics huggingface dataset:
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) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

pp: case succ.e_a.refine_2
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)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
·

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) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_2
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)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
·

Goal state after:
case succ.e_a.refine_2
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)
⊢ n.choose 0 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : ¬p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case isTrue
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : p = 0
⊢ 0 = 0

pp: case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Tactic:
·

Goal state after:
case isTrue
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : p = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

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

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

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : Ring R
r a : R
h✝ : Subsingleton R
⊢ rootMultiplicity a (C r) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0

pp: case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree

Tactic:
·

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨅ i, l i → ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
·

Goal state after:
case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨅ i, l i → ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree

Tactic:
·

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
·

Goal state after:
case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t) → t ∈ ⨅ i, l i
Module: Mathlib.Algebra.Polynomial.Div

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

pp: case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
·

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

Goal state before:
pp: case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
·

Goal state after:
case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ 1 ≤ p.natDegree

Tactic:
by lia

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : t ∈ ⨅ i, l i
⊢ ∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t

pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : t ∈ ⨅ i, l i
⊢ ∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
hp : derivative 0 = 0
⊢ natDegree 0 = 0

pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
⊢ p.natDegree = 0

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
hp : derivative 0 = 0
⊢ natDegree 0 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : derivative p = 0
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
⊢ 1 ≤ p.natDegree

Tactic:
by lia

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

Goal state before:
pp: case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

pp: case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
·

Goal state after:
case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.left
α : Type u_1
s : ℕ → Set α
⊢ Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m

pp: case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
·

Goal state after:
case h.left
α : Type u_1
s : ℕ → Set α
⊢ Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

pp: case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
·

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x

Tactic:
rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]

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

Goal state before:
pp: case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
·

Goal state after:
case a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

pp: case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
·

Goal state after:
case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
·

Goal state after:
case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree
Module: Mathlib.Order.Filter.Finite

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

pp: case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i

Tactic:
·

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ U ∈ ⨅ i, s i → ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ p.natDegree ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x

pp: case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Tactic:
·

Goal state after:
case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Tactic:
·

Goal state after:
case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

pp: case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos.inl
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

pp: case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
·

Goal state after:
case pos.inl
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
·

Goal state after:
case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : ¬q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

pp: case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : ¬q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)

Tactic:
·

Goal state after:
case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)

Tactic:
·

Goal state after:
case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff

pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Finite

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

Tactic:
·

Goal state after:
case mpr
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
⊢ (∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) → U ∈ ⨅ i, s i
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Tactic:
·

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i

pp: case refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

pp: case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Tactic:
·

Goal state after:
case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i ∈ s i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ

pp: case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Tactic:
·

Goal state after:
case refine_2
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
hi : i ∉ I
⊢ (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i = univ
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i

Tactic:
·

Goal state after:
case refine_3
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, V i = ⋂ x, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) ↑x ∧
    ⋂ i, V i = ⋂ i, (fun i ↦ if hi : i ∈ I then V ⟨i, hi⟩ else univ) i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i) → ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

pp: case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) → t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
·

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i) → ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
Module: Mathlib.Algebra.Polynomial.Div

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

pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ (n + 1) ∣ p

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ 0 ∣ p