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

Goal state before:
pp: case zero
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
⊢ s ↑(x 0) ∈ f

pp: case succ
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
n✝ : ℕ
⊢ s ↑(x (n✝ + 1)) ∈ f

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
⊢ s ↑(x 0) ∈ f

case succ
α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
x' : ℕ → Set α
hx' : f = ⨅ i, 𝓟 (x' i)
this✝ : ∀ (i : ℕ), x' i ∈ f
x : ℕ → { i // p i } := fun n ↦ Nat.recOn n (hs.index (x' 0) ⋯) fun n xn ↦ hs.index (x' (n + 1) ∩ s ↑xn) ⋯
x_anti : Antitone fun i ↦ s ↑(x i)
x_subset : ∀ (i : ℕ), s ↑(x i) ⊆ x' i
this : (⨅ i, 𝓟 (s ↑(x i))).HasAntitoneBasis fun i ↦ s ↑(x i)
n✝ : ℕ
⊢ s ↑(x (n✝ + 1)) ∈ f
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hi : j ∈ I
x : α j
hx : x ∈ t j
⊢ update g j x j ∈ t j

pp: case inr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hne : j ≠ i
⊢ update g i x j ∈ t j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hi : j ∈ I
x : α j
hx : x ∈ t j
⊢ update g j x j ∈ t j

case inr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
hne : j ≠ i
⊢ update g i x j ∈ t j
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ (s ∈ pi fun i ↦ pure (f i)) ↔ ∃ I, I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s

Tactic:
simp only [← principal_singleton, mem_pi_principal]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ (I.pi fun i ↦ {f i}) ⊆ s) ↔ ∃ I, I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s
Module: Mathlib.Algebra.Polynomial.Div

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

pp: case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∉ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
<;>

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

case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∉ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Algebra.Polynomial.Derivative

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

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

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case inl.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a

pp: case inl.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a

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

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

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 inl.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a

case inl.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a

case inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

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

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

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

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

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

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

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

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

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

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

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

case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

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

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

case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Module: Mathlib.Order.Heyting.Boundary

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

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

Tactic:
<;>

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

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 β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
rw [prod_comm]; rfl

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

Goal state before:
pp: case refine_1
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.fst ⁻¹' m₁ ⁻¹' u₁
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.fst ⁻¹' u₁

pp: case refine_2
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.snd ⁻¹' m₂ ⁻¹' u₂
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.snd ⁻¹' u₂

Tactic:
<;>

Goal state after:
case refine_1
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.fst ⁻¹' m₁ ⁻¹' u₁
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.fst ⁻¹' u₁

case refine_2
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.snd ⁻¹' m₂ ⁻¹' u₂
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.snd ⁻¹' u₂
Module: Mathlib.Algebra.Polynomial.Derivative

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

pp: case succ
R : Type u
inst✝ : Ring R
n : ℤ
n✝ : ℕ
a✝ : ∀ {f : R[X]}, (⇑derivative)^[n✝] (↑n * f) = ↑n * (⇑derivative)^[n✝] f
f : R[X]
⊢ (⇑derivative)^[n✝ + 1] (↑n * f) = ↑n * (⇑derivative)^[n✝ + 1] f

Tactic:
<;>

Goal state after:
case zero
R : Type u
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ (⇑derivative)^[0] (↑n * f) = ↑n * (⇑derivative)^[0] f

case succ
R : Type u
inst✝ : Ring R
n : ℤ
n✝ : ℕ
a✝ : ∀ {f : R[X]}, (⇑derivative)^[n✝] (↑n * f) = ↑n * (⇑derivative)^[n✝] f
f : R[X]
⊢ (⇑derivative)^[n✝ + 1] (↑n * f) = ↑n * (⇑derivative)^[n✝ + 1] f
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ s.prod = x * (y * k)

Tactic:
· rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
        left; exact hprod

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ normalizedFactors a = {normalize a}

Tactic:
obtain ⟨p, a_assoc, hp⟩ :=
    prime_factors_irreducible ha ⟨prime_of_normalized_factor, prod_normalizedFactors ha.ne_zero⟩
  have p_mem : p ∈ normalizedFactors a := by
    rw [hp]
    exact Multiset.mem_singleton_self _
  convert! hp
  rwa [← normalize_normalized_factor p p_mem, normalize_eq_normalize_iff, dvd_dvd_iff_associated]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case e'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = normalize p

pp: case e'_3
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ q = normalize q

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = normalize p

case e'_3
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ q = normalize q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
hp : p = 0
⊢ (C a * p).roots = p.roots

pp: case neg
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (C a * p).roots = p.roots

Tactic:
<;>

Goal state after:
case pos
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
hp : p = 0
⊢ (C a * p).roots = p.roots

case neg
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
hp : ¬p = 0
⊢ (C a * p).roots = p.roots
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case h
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ Finset.univ

pp: case hf
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∀ x ∈ Finset.univ, x ∉ f.support → f x = 0

Tactic:
<;>

Goal state after:
case h
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ Finset.univ

case hf
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∀ x ∈ Finset.univ, x ∉ f.support → f x = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case hf.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝¹ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx✝ : x ∈ normalizedFactors x✝ + normalizedFactors y
hx : x ∈ normalizedFactors x✝
⊢ Irreducible x

pp: case hf.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝¹ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx✝ : x ∈ normalizedFactors x✝ + normalizedFactors y
hx : x ∈ normalizedFactors y
⊢ Irreducible x

Tactic:
<;>

Goal state after:
case hf.inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝¹ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx✝ : x ∈ normalizedFactors x✝ + normalizedFactors y
hx : x ∈ normalizedFactors x✝
⊢ Irreducible x

case hf.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x✝ y : α
hx✝¹ : x✝ ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
x : α
hx✝ : x ∈ normalizedFactors x✝ + normalizedFactors y
hx : x ∈ normalizedFactors y
⊢ Irreducible x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ.zero
σ : Type u_5
s : Set ℕ
hn : 0 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((0 + 1) • s) = (0 + 1) • ⇑degree ⁻¹' s

pp: case succ.succ
σ : Type u_5
s : Set ℕ
n✝ : ℕ
a✝ : n✝ + 1 ≠ 0 → ⇑degree ⁻¹' ((n✝ + 1) • s) = (n✝ + 1) • ⇑degree ⁻¹' s
hn : n✝ + 1 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n✝ + 1 + 1) • s) = (n✝ + 1 + 1) • ⇑degree ⁻¹' s

Tactic:
<;>

Goal state after:
case succ.zero
σ : Type u_5
s : Set ℕ
hn : 0 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((0 + 1) • s) = (0 + 1) • ⇑degree ⁻¹' s

case succ.succ
σ : Type u_5
s : Set ℕ
n✝ : ℕ
a✝ : n✝ + 1 ≠ 0 → ⇑degree ⁻¹' ((n✝ + 1) • s) = (n✝ + 1) • ⇑degree ⁻¹' s
hn : n✝ + 1 + 1 ≠ 0
⊢ ⇑degree ⁻¹' ((n✝ + 1 + 1) • s) = (n✝ + 1 + 1) • ⇑degree ⁻¹' s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors x) (factors x)

Tactic:
exact rel_refl_of_refl_on fun y _ => Associated.refl _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : ¬p.coeff n ≠ 0
⊢ p.content ∣ p.coeff n

Tactic:
Classical.not_not

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

pp: case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

pp: case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.calc_2.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x

pp: case neg.calc_2.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x

Tactic:
<;>

Goal state after:
case neg.calc_2.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x

case neg.calc_2.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h✝ : ¬b = 0
cne0 : c ≠ 0
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝

Tactic:
<;>

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝