mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]}, q ^ n ∣ p → q ^ (n - m) ∣ (⇑derivative)^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - m).pred ∣ (⇑derivative ∘ (⇑derivative)^[m]) p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ ↑n * eval c ((⇑derivative)^[m] (f ^ (n - 1) * derivative f))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = U

pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, ⋂₀ σ i ⊆ U

Tactic:
]

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ ⋂ i, ⋂₀ σ i ⊆ U
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ X ^ n = X ^ n

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ x, eval ↑x ⁻¹' s ↑x ∈ pi f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval t g = eval t g

Tactic:
]

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

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

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(n.descFactorial k) * X ^ (n - (k + 1))
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ C ↑(n.descFactorial k) * X ^ (n - k) = C ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) = C ↑m * (X + C c) ^ (m - 1)

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) = C 2 * (X + C c)

Tactic:
]

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
]

Goal state after:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = eval t g

Tactic:
]

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

Goal state before:
pp: case right
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
w✝ : Set ↑(range f)
left✝² : w✝.Finite
V : ↑(range f) → Set α
hVs : ∀ (i : ↑(range f)), V i ∈ ↑i
left✝¹ : ∀ i ∉ w✝, V i = univ
left✝ : s = ⋂ i ∈ w✝, V i
hVU' : s = ⋂ i, V i
⊢ ⋂ x, V (rangeFactorization f x) = ⋂ i, (fun x ↦ V (rangeFactorization f x)) i

Tactic:
]

Goal state after:
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 ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
]

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 ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
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
⊢ 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
⊢ 1 ∣ p
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i : Set ι × (ι → κ)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
      ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)

Tactic:
rintro ⟨I, k⟩ ⟨hI, hk⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
I : Set ι
k : ι → κ
hI : (I, k).1.Finite
hk : ∀ i ∈ (I, k).1, p ((I, k).2 i)
⊢ ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ (I, k).1.pi fun i ↦ s i ((I, k).2 i)
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
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
]

Goal state after:
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
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ rootMultiplicity a p ≤ n

Tactic:
]

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i' : Set ι × κ),
    i'.1.Finite ∧ p i'.2 →
      ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ i'.1.pi fun i ↦ s i i'.2

Tactic:
rintro ⟨I, k⟩ ⟨hI, hk⟩

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
I : Set ι
k : κ
hI : (I, k).1.Finite
hk : p (I, k).2
⊢ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ (I, k).1.pi fun i ↦ s i (I, k).2
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
s : (i : ι) → Set (α i)
⊢ (pi fun i ↦ 𝓟 (s i)) = 𝓟 (univ.pi s)

Tactic:
simp [Filter.pi, Set.pi_def]

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

Goal state before:
pp: α : Type u
ι : Type u_2
f : ι → Filter α
⊢ ⋃ i, (⨅ i_1 ∈ i, f i_1).sets = ⋃ t, (⨅ i ∈ t, f i).sets

pp: case h
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun t ↦ ⨅ i ∈ t, f i

Tactic:
]

Goal state after:
case h
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun t ↦ ⨅ i ∈ t, f i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ x, f x.down).sets = (⨅ i, f i.down).sets

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
⊢ rootMultiplicity a p ≤ rootMultiplicity a p

Tactic:
]

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

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Tactic:
]

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0

Tactic:
]

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0
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 ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ 𝓟 (f i ∩ ⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)

Tactic:
]

Goal state after:
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
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

Goal state after:
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
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p /ₘ q).leadingCoeff

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).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:
]

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.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
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree
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:
]

Goal state after:
α : 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
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₂ : 1 = 0
⊢ p.degree = 1

Tactic:
]

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.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ f i

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
I : Set ι
hIf : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hI : eval i '' I.pi t ⊆ s
⊢ s ∈ 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:
]

Goal state after:
α : 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
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x

Tactic:
]

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x

Tactic:
]

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x
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
hgu : IsUnit g
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ leadingCoeff 0 = leadingCoeff 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ 𝓟 t, t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1 ∈ f, t_1 ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ {a | ∀ b ∈ univ, (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ 0 < p.degree

Tactic:
]

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ 0 < p.degree
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ⊥ = ⊥

Tactic:
]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b = a ⊓ ￢a ⊓ b ⊔ a ⊓ b ⊓ ￢b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ comap Prod.fst f = comap Prod.fst f

Tactic:
]

Goal state after:
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 ∣ q

Tactic:
]

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 ∣ q
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ comap Prod.snd g = comap Prod.snd g

Tactic:
]

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
hq : IsUnit q.leadingCoeff
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : IsUnit q.leadingCoeff
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = q

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)

Tactic:
]

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

Goal state before:
pp: case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)

Tactic:
]

Goal state after:
case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)