mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
{ exact le_sup_of_le_left inf_le_left }

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative)^[n + 1 + 1 + 2] p * X ^ 2 + (2 * (n + 1 + 1)) • (⇑derivative)^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative)^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative)^[n + 1 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ f ×ˢ ⨅ i, g i = ⨅ i, f ×ˢ g i

Tactic:
by

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

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p ↦ (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
{ exact le_sup_of_le_left inf_le_left }

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
⊢ derivative (p.comp q) = derivative q * (derivative p).comp q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
by

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

Goal state before:
pp: α : Type u_2
⊢ cofinite = ⊥ ↔ Finite α

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (eval₂ C q (C r)) = eval₂ C q (derivative (C r)) * derivative q

Tactic:
by

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

Goal state before:
pp: α : Type u_2
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ {x | p x}.Infinite

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
inst✝ : g.NeBot
p : α → β → Prop
q : β → γ → Prop
r : α → γ → Prop
hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y
hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z
hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z
⊢ ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set (α × β)
⊢ sᶜ ∈ cofinite.coprod cofinite ↔ sᶜ ∈ cofinite

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i ↦ cofinite) ↔ sᶜ ∈ cofinite

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
⊢ l.kerᶜ.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (f ⁻¹' l.ker)ᶜ.Countable

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
s : (i : ι) → Set (α i)
l : (i : ι) → Filter (α i)
h : ∀ (i : ι), s i ∈ l i
hfin : ∀ᶠ (i : ι) in cofinite, s i = univ
⊢ univ.pi s ∈ pi l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ a \ ∂ a = ￢￢a

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ derivative (eval₂ C q (p₁ + p₂)) = eval₂ C q (derivative (p₁ + p₂)) * derivative q

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' (s + t) = ⇑ofAdd '' s * ⇑ofAdd '' t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
n : ℕ
s : Set M
⊢ ⇑ofAdd '' (n • s) = (⇑ofAdd '' s) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set (Multiplicative M)
⊢ ⇑toAdd '' (s * t) = ⇑toAdd '' s + ⇑toAdd '' t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
n : ℕ
s : Set (Multiplicative M)
⊢ ⇑toAdd '' s ^ n = n • ⇑toAdd '' s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
by

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

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
F : Filter α
G : Filter γ
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
⊢ map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst✝ : Finite ι
f : (i : ι) → α i → β i
l : (i : ι) → Filter (α i)
⊢ ∀ᶠ (i : ι) in cofinite, Surjective (f i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = (map (fun a b ↦ m (a, b)) f).seq g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
f₁ f₂ : Filter α
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Tactic:
by

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

Goal state before:
pp: ⊢ cofinite = atTop

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ {n | p n}.Infinite

Tactic:
by

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

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

Tactic:
rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ f ×ˢ pure b = map (fun a ↦ (a, b)) f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ derivative (Multiset.map f 0).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (Multiset.erase 0 i)).prod * derivative (f i)) 0).sum

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f ×ˢ g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
f' : Filter α
g' : Filter β
⊢ Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Tactic:
by

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ update f a b =ᶠ[𝓟 {a}ᶜ] f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ cofinite ≤ 𝓟 {a}ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → β
inst✝ : Zero β
⊢ Tendsto f cofinite (pure 0) ↔ HasFiniteSupport f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n ↦ (s n).1) f g ∧ Tendsto (fun n ↦ (s n).2) f g'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
f : Filter α
x : α
h : {x}ᶜ ∈ f
⊢ x ∉ {x}ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ ⊥.coprod ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ la.coprod lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Tactic:
by

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ f.ker = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ ⊤ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
by

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

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
x : α
hx : x ∈ f.ker
⊢ False

Tactic:
exact hx f.kerᶜ h hx

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f

Tactic:
by

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

Goal state before:
pp: α : Type u_2
s : Set α
⊢ Coheyting.boundary (𝓟 s) = ⊥

Tactic:
by

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

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (map m₁ f₁).coprod (map m₂ f₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ (map (fun x ↦ b) (𝓟 {a})).coprod (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})

Tactic:
by

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

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x ↦ b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)

Tactic:
by

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 ∈ la, Tendsto f (𝓟 sᶜ ×ˢ lb) lc
h₂ : Tendsto f (la ×ˢ ⊤) lc
⊢ Tendsto f (la.coprod lb) lc

Tactic:
by

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

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum

Tactic:
by

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Finset ι
f : ι → R[X]
⊢ derivative (∏ b ∈ s, f b) = ∑ a ∈ s, (∏ b ∈ s.erase a, f b) * derivative (f a)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ derivative (X - C c) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative ↑n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
k : ℕ
f : R[X]
⊢ (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ derivative (p.comp (1 - X)) = -(derivative p).comp (1 - X)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (p.comp (1 - X)) = (-1) ^ k * ((⇑derivative)^[k] p).comp (1 - X)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ ∃! p, p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2

Tactic:
by

Goal state after:
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
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) S).prod) = (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
⊢ derivative ((X - C c) ^ 2) = C 2 * (X - C c)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative)^[k] ((X - C c) ^ n) = n.descFactorial k • (X - C c) ^ (n - k)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ (⇑derivative)^[n] ((X - C c) ^ n) = ↑n !

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : ¬derivative P = 0
⊢ P.natDegree ≠ 0

Tactic:
by

Goal state after: