mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ys : List α
ih : (∀ x ∈ ys, x ∈ xs') → ys.nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: ys, x ∈ xs'
⊢ (y :: ys).nextOr x d ∈ xs'

Tactic:
rcases ys with - | ⟨z, zs⟩

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ih : (∀ x ∈ [], x ∈ xs') → [].nextOr x d ∈ xs'
hxs' : ∀ x ∈ [y], x ∈ xs'
⊢ [y].nextOr x d ∈ xs'

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
⊢ (y :: z :: zs).nextOr x d ∈ xs'
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
hf : Function.Injective ⇑f
⊢ Nat.card α ∣ Nat.card H

Tactic:
by
  calc
      Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
      _ ∣ Nat.card H := card_subgroup_dvd_card _

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

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
refine ⟨fun _ => Ne.symm hx.left, ?_⟩

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : 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
⊢ (x :: l).permutations'.Nodup

Tactic:
| @cons x l h h' IH =>

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ ¬s.permutations.Nodup

Tactic:
rw [duplicate_iff_sublist] at hs

Goal state after:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
⊢ ¬s.permutations.Nodup
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α), x ∈ fixedPoints G α

Tactic:
simp only [mem_fixedPoints]

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Subsingleton α
⊢ ∀ (x : α) (m : G), m • x = x
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
⊢ orbitRel (↥(H.subgroupOf K)) α = orbitRel (↥(H ⊓ K)) α

Tactic:
by
  rw [← Subgroup.subgroupOf_map_subtype]
  ext x
  simp_rw [orbitRel_apply]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only
    refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))
    simpa using! gp
  · rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only
    simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
    refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
    · exact gp.2
    · simp only [Subgroup.mem_subgroupOf]
      exact gp.1

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

Goal state before:
pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
exact le_of_dvd hn (dvd_of_mem_primeFactorsList h)

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card ↑(MulAction.orbit (ConjAct G) g)

Tactic:
ConjAct.orbit_eq_carrier_conjClasses

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (L.subtype.range ⊓ J).relIndex (K ⊓ L.subtype.range) ≠ 0

Tactic:
← map_comap_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (K ⊓ L.subtype.range) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (L.subtype.range ⊓ K) ≠ 0

Tactic:
← map_comap_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (map L.subtype (comap L.subtype K)) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
n : ℕ
nzm : NeZero 0
h : 0 ≤ n
⊢ Injective cast

Tactic:
cases nzm; simp_all

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R : Type u
M' : Type v
inst✝¹ : Semiring R
inst✝ : Fintype M'
⊢ #R[M'] = lift.{v, u} #R ^ card M'

Tactic:
by
  simp [coeffEquiv.cardinal_eq]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
grw [← hx]
      gcongr
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

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

Goal state before:
pp: case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
simpa [ZMod.val_add] using! Nat.mod_le _ _

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n ∧ 0 = x + 1 ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
Decidable.and_or_imp,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n → 0 = x + 1 ∨ 0 < x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Tactic:
by
  rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x y z : ℤ
hz : z ≠ 0
⊢ (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Tactic:
by
  simp [hz]

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

Goal state before:
pp: n : ℕ
⊢ padicValNat 0 n = 0

Tactic:
by simp [padicValNat]

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

Goal state before:
pp: n : ℕ
⊢ padicValNat 1 n = 0

Tactic:
by simp [padicValNat]

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

Goal state before:
pp: p : ℕ
⊢ padicValNat p 0 = 0

Tactic:
by simp [padicValNat]

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

Goal state before:
pp: p : ℕ
⊢ padicValNat p 1 = 0

Tactic:
by simp [padicValNat]

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

Goal state before:
pp: case inl
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n

Tactic:
rcases k.eq_zero_or_pos with rfl | hk <;> simp [Nat.ne_of_gt, *]

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

Goal state before:
pp: case nil
b : ℕ
l2 : List ℕ
h : [].length = l2.length
⊢ ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) [] l2)

Tactic:
simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
by_cases hf : FiniteMultiplicity a b

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ ↑(multiplicity a b) ≤ emultiplicity a b
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by_contra! nh; simp [nh] at h

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
by_cases hf : FiniteMultiplicity a b

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
refine ⟨c, hc, ?_⟩

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ¬a ∣ c
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n ≤ count p n.primeFactorsList

Tactic:
← Nat.lt_add_one_iff,

Goal state after:
case a
n p : ℕ
hn0 : n > 0
pp : Prime p
⊢ padicValNat p n < count p n.primeFactorsList + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1

Tactic:
by
  simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
  split_ifs with h1
  · classical
    rw [find_eq_iff]
    simp only [h, true_and, not_and]
  · rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ ∀ (a : α) (s : Finset α),
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization = ∑ x ∈ s, (g x).factorization →
            ((insert a s).prod g).factorization = ∑ x ∈ insert a s, (g x).factorization

Tactic:
· intro x T hxS hTS hxT IH
      have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
      simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a

Tactic:
simp only [pow_one, dvd_refl, reduceAdd, true_and]

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ ¬a ^ 2 ∣ a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a)).Finite

Tactic:
rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

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

Goal state before:
pp: x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ x / p / p ^ (x / p).factorization p = x / p ^ x.factorization p

Tactic:
by
  simpa [pow_one] using ordCompl_div_pow_of_dvd 1 hp (show p ^ 1 ∣ x by simpa)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
h' : y ∈ zpowers x
⊢ IsOfFinOrder y

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'
  exact h.zpow

Goal state after:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 0) x = x

Tactic:
rw [iterateFrobenius_def, pow_zero, pow_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h)

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = 1 ∧ l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

case inr
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h✝ : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
h : k = -1 ∧ l = -1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) + emultiplicity p k ≤ ↑n

Tactic:
have hdisj :
        Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
          {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
        simp +contextual [disjoint_right, *, dvd_iff_mod_eq_zero,
          Nat.mod_lt _ (pow_pos hp.pos _)]
      rw [emultiplicity_choose hp hkn (lt_succ_self _),
        emultiplicity_eq_card_pow_dvd (ne_of_gt hp.one_lt) hk0.bot_lt
          (lt_succ_of_le (log_mono_right hkn)),
        ← Nat.cast_add]
      apply WithTop.coe_mono
      rw [log_pow hp.one_lt, ← card_union_of_disjoint hdisj, filter_union_right]
      have filter_le_Ico := (Ico 1 n.succ).card_filter_le
        fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
      rwa [card_Ico 1 n.succ] at filter_le_Ico

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

Tactic:
rintro ⟨x, rfl⟩
    rw [of'_mul_modOf]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.divX * X + C (p.coeff 0)).coeff 0 = p.coeff 0

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.divX * X + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X * p.divX + C (p.coeff 0)).coeff 0 = p.coeff 0

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (X * p.divX + C (p.coeff 0)).coeff (n✝ + 1) = p.coeff (n✝ + 1)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree
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
⊢ g • a = a

Tactic:
by
  have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))
  rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
  exact le_antisymm h key

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ ↑(card R) = 0

Tactic:
← nsmul_one,

Goal state after:
R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ card R • 1 = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
⊢ ↑p ^ i = 0

Tactic:
by rw [← Nat.cast_pow, CharP.cast_eq_zero]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree < o

Tactic:
apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ (p ^ m).natDegree ≤ m * n

R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ p.leadingCoeff ^ (q.natDegree + 1) = 1

Tactic:
simp [show _ = _ from hmp]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by_cases hp : p = 0
  · rw [hp, zero_mul, trailingDegree_zero, top_add]
  by_cases hq : q = 0
  · rw [hq, mul_zero, trailingDegree_zero, add_top]
  · rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
    apply WithTop.coe_add

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
· rw [modByMonic_eq_of_not_monic p hq]

Goal state after:
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
a : R
| rootMultiplicity a p

Tactic:
← mul_divByMonic_eq_iff_isRoot.mpr hx

Goal state after:
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
a : R
| rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Tactic:
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ degree 0 < ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: 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
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
by
  by_cases hp : p = 0
  · convert! hq
    simp [hp, cancelLeads]
  rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
  by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
  · exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq
  apply lt_of_le_of_ne
  · compute_degree!
    rwa [Nat.sub_add_cancel]
  · contrapose h0
    rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]
    simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
    rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]

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

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

Tactic:
le_iInf_iff

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

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

Tactic:
le_iInf_iff

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ (⨅ i, f i).IsCountablyGenerated

Tactic:
rw [← PLift.down_surjective.iInf_comp]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
s : ι → ℕ → Set α
hs : ∀ (i : ι), (f i).HasAntitoneBasis (s i)
⊢ (⨅ x, f x.down).IsCountablyGenerated
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ i, f i
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
← iInf_range' (g := (·))

Goal state after:
ι : Sort u_2
α : Type u_3
f : ι → Filter α
s : Set α
hs : s ∈ ⨅ b, ↑b
⊢ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
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:
· exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset M
a : M
s : Multiset M
ih : (Multiset.map Associates.mk s).prod = Associates.mk s.prod
⊢ (Multiset.map Associates.mk (a ::ₘ s)).prod = Associates.mk (a ::ₘ s).prod

Tactic:
simp [ih, Associates.mk_mul_mk]

Goal state after: