mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Prod

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

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ Prod.swap ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
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 ∘ Prod.swap) (g ×ˢ f) = g

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : f.NeBot
⊢ map (Prod.snd ∘ Prod.swap) (g ×ˢ f) = g
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Tactic:
]

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ b ≤ ∂ (b ⊔ a) ⊔ ∂ (b ⊓ a)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l

Tactic:
]

Goal state after:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ∀ i ∈ sᶜ, {i}ᶜ ∈ l
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
]

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

Goal state before:
pp: α : Type u_2
l : Filter α
inst✝ : l.IsCountablyGenerated
h : cofinite ≤ l
s : ℕ → Set α
hs : l.HasAntitoneBasis s
⊢ (⋃ i, (s i)ᶜ).Countable

Tactic:
exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

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
⊢ (comap f l).kerᶜ.Countable

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ≤ a
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a
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
⊢ eval₂ C q (derivative p₁) * derivative q + eval₂ C q (derivative p₂) * derivative q =
    eval₂ C q (derivative p₁) * derivative q + eval₂ C q (derivative p₂) * derivative q

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (univ.pi fun i ↦ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
]

Goal state after:
ι : 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
⊢ (univ.pi fun i ↦ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i) ∈ pi fun i ↦ map (f i) (l i)
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

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

Tactic:
]

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 + ⇑toAdd '' t = ⇑toAdd '' s + ⇑toAdd '' t

Tactic:
]

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
⊢ s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s

Tactic:
]

Goal state after:
α₁ : 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
⊢ s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
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 f F ×ˢ G

Tactic:
]

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 = F ×ˢ map f G

Tactic:
]

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
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Tactic:
]

Goal state after:
α : 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
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
Module: Mathlib.Order.Filter.Cofinite

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

Tactic:
]

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₁ ⊓ f₂) ×ˢ g

Tactic:
]

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₁ ⊓ g₂)

Tactic:
]

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

Goal state before:
pp: p : ℕ → Prop
⊢ {x | p x}.Infinite ↔ {n | p n}.Infinite

Tactic:
]

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
⊢ eval₂ C q (derivative (C r * X ^ n)) * q * derivative q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n)) * q * derivative q + eval₂ C q (C r * X ^ n) * derivative q

Tactic:
]

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

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

Tactic:
]

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) (map (Prod.mk a) B) = map (f a) B

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g ↦ g b) ∘ Prod.mk) f = map (fun a ↦ (a, b)) f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map ((fun g ↦ g b) ∘ Prod.mk) f = map (fun a ↦ (a, b)) f
Module: Mathlib.Order.Filter.Prod

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

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ i, ∃ (_ : i ∈ f), a ∉ i

Tactic:
]

Goal state after:
α : Type u_2
f : Filter α
⊢ (∀ (x : α), {x}ᶜ ∈ f) ↔ ∀ (a : α), ∃ i, ∃ (_ : i ∈ f), a ∉ i
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₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ ∀ (x : α), x ∉ f.ker

Tactic:
]

Goal state after:
case mpr
α : Type u_2
f : Filter α
h : f.kerᶜ ∈ f
⊢ ∀ (x : α), x ∉ f.ker
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t)

Tactic:
]

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]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
]

Goal state after:
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_2
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2
Module: Mathlib.Order.Filter.Prod

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

Tactic:
]

Goal state after:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
]

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map (HMul.hMul (f i)) (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_3
α : Type u_2
f : Filter α
⊢ f = f

Tactic:
]

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

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

Tactic:
]

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ (Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
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 = (f.ker, Coheyting.boundary f)

Tactic:
]

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.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_1
α : 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 ≤ 𝓟 q.1 ⊔ q.2

Tactic:
]

Goal state after:
case refine_4.refine_1
α : 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 ≤ 𝓟 q.1 ⊔ q.2
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_2
α : 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
⊢ Disjoint (𝓟 q.1) q.2

Tactic:
]

Goal state after:
case refine_4.refine_2
α : 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
⊢ Disjoint (𝓟 q.1) q.2
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative (C ↑n) = 0
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4.refine_3
α : 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
⊢ Coheyting.boundary q.2 ≤ q.2

Tactic:
]

Goal state after:
case refine_4.refine_3
α : 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
⊢ Coheyting.boundary q.2 ≤ q.2
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) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
]

Goal state after:
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) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a ↦ r - a) (S.erase r)).prod
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing 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✝ : CommRing R
c : R
⊢ C 2 * (X - C c) = C 2 * (X - C c)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ ↑n ! = ↑n !

Tactic:
]

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
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
]

Goal state after:
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
⊢ (⇑derivative)^[k] (derivative P) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑k ! * (↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑k ! * (↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a))
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : f ⁻¹' {i} = ∅
⊢ mapDomain f v i = 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : f ⁻¹' {i} = ∅
⊢ mapDomain f v i = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ p ∈ ?r, ∏ a ∈ p.1.erase p.2, (X - C a) =
    ∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)

pp: case r
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ Finset (Finset R × R)

pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (p : Finset R × R), p ∈ ?r ↔ p.1 ∈ powersetCard (#S - k) S ∧ p.2 ∈ p.1

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (p : Finset R × R),
    p ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T} ↔
      p.1 ∈ powersetCard (#S - k) S ∧ p.2 ∈ p.1
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: case refine_1
α : 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
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree y

Tactic:
]

Goal state after:
case refine_1
α : 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
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree y
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)

Tactic:
]

Goal state after:
R : Type ?u.3
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ Associated (a * b) (a * b)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
]

Goal state after:
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q