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

Goal state before:
pp: case mem.add
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 : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n]^[minimalPeriod f x / (minimalPeriod f x).gcd n] x = x

Tactic:
← iterate_mul,

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ f^[n * (minimalPeriod f x / (minimalPeriod f x).gcd n)] x = x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ

Tactic:
Nat.mul_succ,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ (ts.permutationsAux (t :: is)).length + (is.length * is.length ! + is.length !) =
    (ts.permutationsAux (t :: is)).length + (is.length ! * is.length + is.length !)
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.add
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 : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r : R
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p x✝ ((algebraMap R A) r) hx✝ ⋯
h₂ : p y✝ ((algebraMap R A) r) hy✝ ⋯
⊢ p (x✝ + y✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
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 : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : a ∈ adjoin R s
x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p a x✝ ha hx✝
h₂ : p a y✝ ha hy✝
⊢ p a (x✝ + y✝) ha ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
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 : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ + y✝, ⋯⟩

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.insertIdx k x = (permutations'Aux x s).get ⟨k + 1, k1l⟩

Tactic:
get_permutations'Aux

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : 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' : (permutations'Aux x as).get ⟨n, hn✝⟩ = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm✝⟩ = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ False

Tactic:
get_permutations'Aux

Goal state after:
case cons.right
α : 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
⊢ False
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mp
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

pp: case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
· rintro ⟨k, hkle, hk_pos, p, hle, heq, hprime⟩
    refine ⟨k, hkle, hk_pos, ?_⟩
    rw [heq, hprime.pow_minFac hk_pos.ne']

Goal state after:
case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
exact fun ⟨a, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod ha1)

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

Goal state before:
pp: case cons.cons.succ
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a : α
l : List α
b : α
m : List α
hn : (a :: l).rotate (d + 1) = b :: m
⊢ IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
hl : l₁.prod = ((b :: l₂).erase a).prod
⊢ a :: l₁ ~ b :: l₂
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
chain_iff_pairwise

Goal state after:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case mk.mk
G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x✝¹ : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ((fun x_1 ↦ (y * x⁻¹) • x_1) x)⁻¹ * y ∈ H

Tactic:
simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]

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

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Tactic:
· exact dvd_zero p

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊥ = 1

Tactic:
by rw [relIndex, subgroupOf_bot_eq_top, index_top]

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

Goal state before:
pp: n : ℕ
⊢ ↑n + 1 = 0

Tactic:
by
  rw [← Nat.cast_add_one, natCast_self (n + 1)]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
exact Int.cast_zero

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

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

Tactic:
cases nzm

Goal state after:
case zero.mk
n : ℕ
h : 0 ≤ n
out✝ : 0 ≠ 0
⊢ Injective cast
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
a : ZMod n
r : R
⊢ a.cast * r = r * a.cast

Tactic:
rcases ZMod.intCast_surjective a with ⟨k, rfl⟩

Goal state after:
R : Type u_1
inst✝¹ : Ring R
n m : ℕ
inst✝ : CharP R m
h : m ∣ n
r : R
k : ℤ
⊢ (↑k).cast * r = r * (↑k).cast
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ 0 < ∑ i ∈ range (n + 1), x ^ i ∧ ∑ i ∈ range (n + 1), x ^ i < 1

Tactic:
geom_sum_succ,

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hmn✝ : 2 ≤ n
ihn : 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1
⊢ 0 < x * ∑ i ∈ range n, x ^ i + 1 ∧ x * ∑ i ∈ range n, x ^ i + 1 < 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : Fact (1 < n)
h : 0 = 1
⊢ 0 = val 0

Tactic:
by rw [val_zero]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)

Tactic:
exact choose_succ_le_two_pow (n - 1) k

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]

Tactic:
rw [Nat.ModEq, ← val_add, neg_add_cancel, tsub_add_cancel_of_le a.val_le, Nat.mod_self,
            val_zero]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ x + x = 0

Tactic:
by
  simpa [two_nsmul] using char_nsmul_eq_zero 2 x

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

Goal state before:
pp: p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ m / p < p * m / p

Tactic:
Nat.mul_div_cancel_left _ hp₀

Goal state after:
p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ m / p < m
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case zero.zero
hm : 0 ≠ 0
⊢ (digits 0 0).getLast ⋯ ≠ 0

pp: case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0

Tactic:
· cases hm rfl

Goal state after:
case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
rw [List.append_assoc, ← digits_base_pow_mul hb hm]

Goal state after:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
cases digits with

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

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ ∀ x ∈ d :: L, x < b

Tactic:
· intro x hx
    obtain rfl | hx := mem_cons.mp hx
    · exact hd
    · exact ((mem_fixedLengthDigits_iff hb).mp hL).2 _ hx

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
rw [fixedLengthDigits_succ_eq_disjiUnion, Finset.sum_disjiUnion]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ i ∈ Finset.range b, ∑ x ∈ consFixedLengthDigits hb l i, x.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
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 [emultiplicity_eq_top.mpr hfin, eq_comm, ENat.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]
    simpa only [FiniteMultiplicity.mul_iff hp, not_and_or] using hfin

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b.factorization ≤ a.factorization
⊢ b ≤ a

Tactic:
factorization_le_iff_dvd hb ha

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
by_cases h : (choose n k).factorization p = 0

Goal state after:
case pos
p n k : ℕ
h : (n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:

Tactic:
x ^ k * x ^ m = x ^ (k + m) := (pow_add _ _ _).symm
        _ = x ^ (m + k) := by simp [Nat.add_comm]
        _ = x ^ m := h
        _ = 1 * x ^ m := by simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1

pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
· simp only [pow_one]

Goal state after:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ ↑(orderOf x) ∣ a - b ↔ x ^ a = x ^ b

Tactic:
orderOf_dvd_iff_zpow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ x ^ (a - b) = 1 ↔ x ^ a = x ^ b
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:
eq_neg_iff_add_eq_zero

Goal state after:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 = 0
Module: Mathlib.Algebra.CharP.Lemmas

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

Tactic:
eq_neg_iff_add_eq_zero

Goal state after:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 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:
CharP.cast_eq_zero

Goal state after:
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
⊢ 0 = 0
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
⊢ False

Tactic:
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp

Goal state after:
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
⊢ False
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (derivative ^ k) (∑ b ∈ s, f b) = ∑ x ∈ s, (derivative ^ k) (f x)

Tactic:
map_sum

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree ≤ g.degree + (q - f /ₘ g).degree

Tactic:
rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ ↑g.natDegree ≤ ↑g.natDegree + ↑(q - f /ₘ g).natDegree
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
⊢ C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0

Tactic:
rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]

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
⊢ (C p.leadingCoeff * q +
          -(C q.leadingCoeff * (p * X ^ (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree)))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
rw [(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr, coeff_zero]
    apply degree_lt_degree; rw [hp, natDegree_X_sub_C]; simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p

Tactic:
by
  suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this
  simp [dvd_iff_isRoot]

Goal state after: