mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
⊢ IsOfFinOrder x → IsOfFinOrder y

Tactic:
by
  simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨n, n_gt_0, eq'⟩
  exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2.inl
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hd : x < b
hx : x ∈ x :: L
⊢ x < b

pp: case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b

Tactic:
· exact hd

Goal state after:
case refine_2.inr
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
x : ℕ
hx✝ : x ∈ d :: L
hx : x ∈ L
⊢ x < b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)

Tactic:
simp [hs, pow_add, mul_comm, mul_left_comm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
· rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]
    norm_cast
    exact multiplicity_mul hp hfin

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
· simp [tsub_eq_zero_of_le]

Goal state after:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n b k : ℕ
hp : Prime p
hkn : k ≤ n
⊢ ∑ i ∈ Ico 1 b, n / p ^ i = ∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i

Tactic:
simp only [add_tsub_cancel_of_le hkn]

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b

pp: case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i < b

Tactic:
· rw [zero_pow, zero_dvd_iff] at h
              exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]

Goal state after:
case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
· rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
a b : G
hab : (a / b) ^ n = 1
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ n, 0 < n ∧ a ^ n = 1
⊢ a / b = 1

Tactic:
exact of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n.factorization m = #({i ∈ Ico 1 b | m ^ i ∣ n})

Tactic:
by
  rwa [factorization_eq_card_pow_dvd n hm, Ico_pow_dvd_eq_Ico_of_lt hm (by lia)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card ↥(zpowers a) ≤ k

Tactic:
rw [Fintype.card_zpowers]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
pow_card_eq_one',

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 ^ (Nat.card G).gcdA n * (g ^ n) ^ (Nat.card G).gcdB n
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = (g ^ Nat.card G) ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
pow_card_eq_one',

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g = 1 ^ (Nat.card G).gcdA n * (g ^ (Nat.card G).gcdB n) ^ n
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g ^ Nat.card G • a
⊢ g • a = a

Tactic:
pow_card_eq_one',

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ 1 • a
⊢ g • a = a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : g ^ Nat.card G • a ≤ g • a
⊢ g • a = a

Tactic:
pow_card_eq_one',

Goal state after:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
key : 1 • a ≤ g • a
⊢ g • a = a
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (p q : R[X]), p.natDegree = 0 ∨ M p → q.natDegree = 0 ∨ M q → (p + q).natDegree = 0 ∨ M (p + q)

pp: case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
· rintro p q (hp | hp) (hq | hq)
    · refine Or.inl ?_
      rw [eq_C_of_natDegree_eq_zero hp, eq_C_of_natDegree_eq_zero hq, ← C_add, natDegree_C]
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hp]
      exact h_C_add hq
    · refine Or.inr ?_
      rw [eq_C_of_natDegree_eq_zero hq, add_comm]
      exact h_C_add hp
    · exact Or.inr (h_add hp hq)

Goal state after:
case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ (f * g).natDegree ≤ df + dg

pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ df + dg ≠ d

Tactic:
· exact natDegree_mul_le_of_le ‹_› ‹_›

Goal state after:
R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
h : ¬d = df + dg
⊢ df + dg ≠ d
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
⊢ (f * g).coeff d = if d = df + dg then a * b else 0

Tactic:
by
  split_ifs with h
  · subst h_mul_left h_mul_right h
    exact coeff_mul_add_eq_of_natDegree_le ‹_› ‹_›
  · apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
    · exact natDegree_mul_le_of_le ‹_› ‹_›
    · exact ne_comm.mp h

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hf : f.degree = 1
hg : g.degree = 0
⊢ IsUnit f

Tactic:
simp [← not_lt, hf, hg] at H

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ p.leadingCoeff * q.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0

Tactic:
comm,

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ q.leadingCoeff * p.leadingCoeff + -(q.leadingCoeff * p.leadingCoeff) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
| p

Tactic:
← modByMonic_add_div p,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
| p %ₘ ?m.80 + ?m.80 * (p /ₘ ?m.80)

R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ R[X]
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

Tactic:
rw [derivative_apply]
    apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
    intro n hn
    apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
    apply le_natDegree_of_mem_supp _ hn

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

Goal state before:
pp: α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
induction is, hf using Set.Finite.induction_on with

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
| p

Tactic:
← modByMonic_add_div p,

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
| p %ₘ ?m.89 + ?m.89 * (p /ₘ ?m.89)

R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
⊢ R[X]
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x

Tactic:
intro h
    exact f.exists_antitone_basis

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

Goal state before:
pp: case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x

pp: case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Tactic:
· intro h
    exact f.exists_antitone_basis

Goal state after:
case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ∃ i, ∃ᶠ (x : α) in l, p i x

Tactic:
rw [← not_iff_not]

Goal state after:
α : Type u
ι : Sort u_2
inst✝ : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ¬∃ i, ∃ᶠ (x : α) in l, p i x
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
rw [← not_iff_not]

Goal state after:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
try { exact le_sup_of_le_left inf_le_left }

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

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

Tactic:
try { exact le_sup_of_le_left inf_le_left }

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

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

Tactic:
try { exact le_sup_of_le_left inf_le_left }

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

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

Tactic:
try { exact le_sup_of_le_left inf_le_left }

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
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:
try { exact le_sup_of_le_left inf_le_left }

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:
try { 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
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_apply]

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:
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]

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

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

Tactic:
disjoint_principal_left

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.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.calc_3
α : 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
⊢ (Classical.choose ⋯).prod * (Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
trans a * c

Goal state after:
α : 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
⊢ (Classical.choose ⋯).prod * (Classical.choose ⋯).prod ~ᵤ a * c

α : 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
⊢ a * c ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ rootSet 0 S = ∅

Tactic:
rw [← C_0, rootSet_C]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ eval t (m.choose b • (m.descFactorial (m - b) • (X - C t) ^ (m - (m - b)) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0

Tactic:
eval_smul,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b • eval t (m.descFactorial (m - b) • (X - C t) ^ (m - (m - b)) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m)) = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b •
      (eval t (m.descFactorial (m - b) • (X - C t) ^ (m - (m - b))) * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0

Tactic:
eval_smul,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b •
      (m.descFactorial (m - b) • eval t ((X - C t) ^ (m - (m - b))) * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
| p.natDegree

Tactic:
rw [he]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
| ((Multiset.map (fun a ↦ X - C a) p.roots).prod * q).natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ ↑a✝ = ⊤

pp: case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝

Tactic:
· rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]

Goal state after:
case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ (a * b).factors = a.factors + b.factors

Tactic:
by
  nontriviality α
  refine FactorSet.unique <| eq_of_factors_eq_factors ?_
  rw [prod_add, factors_prod, factors_prod, factors_prod]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.degree ≠ ⊥

Tactic:
rw [Ne, degree_eq_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ ¬q.primPart = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.degree ≠ ⊥

Tactic:
rw [Ne, degree_eq_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ ¬p.primPart = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ a

Tactic:
apply dvd_of_mk_le_mk

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ b

Tactic:
apply dvd_of_mk_le_mk

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk b