mathlib-initiative/mathlib-tactics huggingface dataset:
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)

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:
·

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 ι × (ι → κ)),
    (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)
Module: Mathlib.Algebra.Polynomial.Div

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

Goal state before:
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 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)
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:
·

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 ι × κ),
    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
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

pp: case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
·

Goal state after:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (univ.pi s) = ⊥ → ∃ i, f i ⊓ 𝓟 (s i) = ⊥

pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (univ.pi s) = ⊥

Tactic:
·

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (univ.pi s) = ⊥ → ∃ i, f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x

Tactic:
·

Goal state after:
case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

pp: case neg
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree
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
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
·

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (univ.pi s) = ⊥

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (univ.pi s) = ⊥
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
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
·

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1

pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n] p * X + n • (⇑derivative)^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ, (n.choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n - k] p * X ^ (1 - k))

Tactic:
·

Goal state after:
case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1

pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative)^[n + 1] p * X + n • (⇑derivative)^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) • ((⇑derivative)^[n - k] (derivative p) * X ^ (1 - k))

Tactic:
·

Goal state after:
case e'_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ X = X ^ 1
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
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

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
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
·

Goal state after:
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
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

pp: case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g
Module: Mathlib.Order.Filter.Prod

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

pp: case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s

Tactic:
·

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s
Module: Mathlib.Algebra.Polynomial.Derivative

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

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

Tactic:
·

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 2] p * X ^ 2 + (2 * 0) • (⇑derivative)^[0 + 1] p * X + (0 * (0 - 1)) • (⇑derivative)^[0] p =
    ∑ k ∈ range (min 2 0).succ,
      (Nat.choose 0 k * Nat.descFactorial 2 k) • ((⇑derivative)^[0 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))
Module: Mathlib.Algebra.Polynomial.Div

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

pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q

Tactic:
·

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

Goal state before:
pp: case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

pp: case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
·

Goal state after:
case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
Module: Mathlib.Algebra.Polynomial.Derivative

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

pp: case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑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:
·

Goal state after:
case succ.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 1 + 2] p * X ^ 2 + (2 * (0 + 1)) • (⇑derivative)^[0 + 1 + 1] p * X +
      ((0 + 1) * (0 + 1 - 1)) • (⇑derivative)^[0 + 1] p =
    ∑ k ∈ range (min 2 (0 + 1)).succ,
      ((0 + 1).choose k * Nat.descFactorial 2 k) • ((⇑derivative)^[0 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))
Module: Mathlib.Order.Heyting.Boundary

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

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

Tactic:
·

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

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

pp: case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q

Tactic:
·

Goal state after:
case add
R : Type u
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : derivative (p✝.comp q) = derivative q * (derivative p✝).comp q
a✝ : derivative (q✝.comp q) = derivative q * (derivative q✝).comp q
⊢ derivative ((p✝ + q✝).comp q) = derivative q * (derivative (p✝ + q✝)).comp q
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q

Tactic:
·

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ derivative (((monomial n✝) a✝).comp q) = derivative q * (derivative ((monomial n✝) a✝)).comp q
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
·

Goal state after:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
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
  refine ⟨fun h => ?_, fun h => h.1 ▸ h.2 ▸ rfl⟩
  have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
  have := neBot_of_le hle.1; have := neBot_of_le hle.2
  exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩

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

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

Tactic:
sup_sdiff_distrib,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a \ ∂ a ⊔ ∂ a \ ∂ a = ￢￢a
Module: Mathlib.Order.Filter.Cofinite

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

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ ∀ᶠ (i : ι) in cofinite, f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i = univ
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s
Module: Mathlib.Order.Filter.Cofinite

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

pp: case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
·

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∃ y ∈ s, ∃ x, f y < x
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Order.Filter.Cofinite

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

Tactic:
·

Goal state after:
case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Order.Filter.Cofinite

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

pp: case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅

Tactic:
·

Goal state after:
case mp
α : 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 α
⊢ f.kerᶜ ∈ f → f.ker = ∅

Tactic:
·

Goal state after:
case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅