mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S✝ : StarSubalgebra R A
f : A →⋆ₐ[R] B
S : StarSubalgebra R A
⊢ ∀ {a : B}, a ∈ (Subalgebra.map (↑f) S.toSubalgebra).carrier → star a ∈ (Subalgebra.map (↑f) S.toSubalgebra).carrier

Tactic:
by
      rintro _ ⟨a, ha, rfl⟩
      exact map_star f a ▸ Set.mem_image_of_mem _ (S.star_mem' ha)

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
⊢ (bs.insertIdx m x)[n] = x

Tactic:
simp [hm', ← hn']

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Tactic:
rw [mem_fixedPoints]
  constructor
  · exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)
  · rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩
    simp only [h]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length

Tactic:
obtain ⟨x, y, hxy, hx, hy⟩ := h
  induction s using Quot.inductionOn with | _ l
  rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
  · simp at hx
  · simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
    simp [hx, hy] at hxy
  · simp [Nat.succ_le_succ_iff]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
· have := isRotated_nil_iff'.1 hab
        contradiction

Goal state after:
case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ primeFactorsList 0 = []

Tactic:
primeFactorsList

Goal state after:
⊢ [] = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ primeFactorsList 1 = []

Tactic:
primeFactorsList

Goal state after:
⊢ [] = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList

Tactic:
primeFactorsList

Goal state after:
n k p : ℕ
h : p ∈ (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).primeFactorsList = [p - 2 + 2]

Tactic:
primeFactorsList

Goal state after:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
primeFactorsList

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

Tactic:
primeFactorsList

Goal state after:
n : ℕ
⊢ (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList =
    (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
primeFactorsList

Goal state after:
case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G), ((MulAction.toPermHom G (G ⧸ H)) g) ↑z = 1 ↑z

Tactic:
refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex K = H.relIndex K

Tactic:
by
  rw [relIndex, relIndex, inf_subgroupOf_right]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H.subgroupOf H).index = 1

Tactic:
subgroupOf_self,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊤.index = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

Tactic:
· apply Fin.val_natCast

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1

Tactic:
exact Int.cast_one

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ ∀ (b : G), b ∈ H

Tactic:
exact fun b ↦ (ha b).elim (fun h ↦ by simpa using mul_mem h (inv_mem ha')) id

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
by
  have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
  exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index * f.ker.index = Nat.card G

Tactic:
index_ker,

Goal state after:
G : Type u_1
inst✝ : Group G
f : G →* G
hf : f.ker.FiniteIndex
⊢ f.range.index * Nat.card ↥f.range = Nat.card G
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ ∈ {1, p}

Tactic:
Finset.mem_insert,

Goal state after:
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ = 1 ∨ a✝ = p ↔ a✝ = 1 ∨ a✝ ∈ {p}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

Tactic:
by
  cases n
  · rw [properDivisors_zero, subset_empty] at hsub
    simp [hsub]
  classical
    rw [← sum_sdiff hsub]
    intro h
    apply Subset.antisymm hsub
    rw [← sdiff_eq_empty_iff_subset]
    contrapose! h
    apply ne_of_lt
    rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
    gcongr
    have hlt :=
      sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
    simp only [sum_const_zero] at hlt
    apply hlt

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
refine ⟨fun h ↦ ?_, Prime.properDivisors⟩

Goal state after:
n : ℕ
h : n.properDivisors = {1}
⊢ Prime n
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑(n.choose k) < ↑n ^ k / ↑k !

Tactic:
rw [lt_div_iff₀' (mod_cast k.factorial_pos)]
  norm_cast
  rw [← Nat.descFactorial_eq_factorial_mul_choose]
  exact descFactorial_lt_pow hn hk

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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Tactic:
induction l1 with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ (↑n * ↑(↑n)⁻¹.val).val = a

Tactic:
ZMod.mul_val_inv hn.symm,

Goal state after:
α : Type u_1
inst✝ : Group α
n : ℕ
a : α
hn : (Nat.card α).Coprime n
⊢ a ^ val 1 = a
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
h : ¬p ∣ n
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
by
  cases n with
  | zero => simp at h
  | succ n => simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]

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

Goal state before:
pp: b k m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m

Tactic:
by
  induction k generalizing m with
  | zero => simp
  | succ k ih =>
    rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]

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

Goal state before:
pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd < p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
apply lt_of_lt_of_le (b := p)

Goal state after:
case succ.cons.hab
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd < p

case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
⊢ 0 < multiplicity a b

Tactic:
refine Nat.pos_iff_ne_zero.2 fun h => ?_

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Tactic:
by
  cases hm : min (emultiplicity p a) (emultiplicity p b)
  · simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
    contrapose hm
    simp only [not_and_or, not_not] at hm ⊢
    exact hm.or_of_add
  · apply le_emultiplicity_of_pow_dvd
    simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

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

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digitsAppend l (ofDigits b L)).length = l

Tactic:
rw [length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Tactic:
simp [pow_add, pow_mul, pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ p ^ k = 1

Tactic:
← hk,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ orderOf x = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p = -1

Tactic:
by
  rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow p]
  rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]; norm_cast

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
· have := Nontrivial.of_polynomial_ne hpq
    exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

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

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

Tactic:
apply hc

Goal state after:
case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 0

case inl.a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p f g : R[X]
hc : IsRelPrime (f.coeff 0 * g.coeff 0) (f.coeff 0 * g.coeff 1)
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ f.coeff 0 ∣ f.coeff 0 * g.coeff 1
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑t.card + 1 ≤ p.degree

Tactic:
by
            rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]
            exact add_le_add (le_refl (1 : WithBot ℕ)) htd

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ p

Tactic:
by rw [← modByMonic_add_div p q, h, zero_add]; exact dvd_mul_right _ _

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

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
le_principal_iff

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⋂ m, ⋂ (_ : m ≤ i), s m ∈ ⨅ i, 𝓟 (s i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mpr
α : Type u
s : Set (Set α)
U : Set α
t : Set (Set α)
hts : t ⊆ s
tfin : t.Finite
h : ⋂₀ t ⊆ U
⊢ U ∈ generate s

Tactic:
exact mem_of_superset ((sInter_mem tfin).2 fun V hV => GenerateSets.basic <| hts hV) h

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
⊢ U ∈ ⨅ i, s i

Tactic:
by
  have := I_fin.fintype
  refine mem_of_superset (iInter_mem.2 fun i => ?_) hU
  exact mem_iInf_of_mem (i : ι) (hV _)

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = ⋂ i, V i

Tactic:
hV,

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
V_in : ∀ (i : ↑I), V i ∈ s ↑i
⊢ U = ⋂ i, (fun i ↦ U ∪ ⋂₀ σ i) i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.h₁
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)

Tactic:
· apply dvd_mul_of_dvd_right
    simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: case h₂
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)

Tactic:
· apply dvd_mul_of_dvd_right
    simp [Polynomial.modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ I.pi s ∈ pi f

Tactic:
pi_def,

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ a ∈ I, eval a ⁻¹' s a ∈ pi f
Module: Mathlib.Order.Filter.Pi

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

Tactic:
by_cases hi : i ∈ I <;> simp [hi, NeBot.ne']

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1 ∈ f, ∃ t₂_1 ∈ g, t₁_1 ×ˢ t₂_1 ⊆ t₁ ∩ t₂

Tactic:
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ⊤ ⊓ ⊥ = ⊥

Tactic:
inf_bot_eq

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ⊥ = ⊥
Module: Mathlib.Order.Filter.Cofinite

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

Tactic:
le_principal_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ comap Prod.fst (𝓟 s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
comap_principal,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
Module: Mathlib.Order.Filter.Prod

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

Tactic:
comap_principal,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s) ⊔ 𝓟 (Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_3
α : Type u_2
f : Filter α
⊢ f = 𝓟 (f.kerᶜᶜ, Coheyting.boundary f).1 ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2

Tactic:
← hnot_principal,

Goal state after:
case refine_3
α : Type u_2
f : Filter α
⊢ f = ￢𝓟 f.kerᶜ ⊔ (f.kerᶜᶜ, Coheyting.boundary f).2
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 * 1 = x * (y * k)

Tactic:
← hk,

Goal state after:
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 * (c * k) = x * (y * k)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod

Tactic:
rwa [add_tsub_cancel_of_le h] at this

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i ↦ (f i).roots

Tactic:
by
  rcases s with ⟨m, hm⟩
  simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n).roots = n • {0}

Tactic:
rw [roots_pow, roots_X]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y → normalizedFactors x ≤ normalizedFactors y

Tactic:
rintro ⟨c, rfl⟩
    simp [hx, right_ne_zero_of_mul hy]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
hx₀ : x ≠ 0
⊢ normalizedFactors x = 0

Tactic:
rwa [normalizedFactors_eq_zero_iff hx₀]

Goal state after: