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

Goal state before:
pp: case cons.mpr
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩

Goal state after:
case cons.mpr.nil
α : Type u_1
t : α
ts : List α
y : α
ys l l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = [] ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ [] ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l_1 ++ l₁ ++ t :: l₂_1 ++ ts
⊢ l ++ [] ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂_1 ++ ts

case cons.mpr.cons
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: l₁ ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
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
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ star a✝ ∈ Algebra.adjoin R (s ∪ star s)

Tactic:
← Subalgebra.mem_star_iff,

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
s : Set A
a✝ : A
hx : a✝ ∈ (Algebra.adjoin R (s ∪ star s)).carrier
⊢ a✝ ∈ star (Algebra.adjoin R (s ∪ star s))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ flatMap (fun y ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
      (map (fun x ↦ x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun a ↦ map (fun x ↦ x ++ ts) (permutationsAux2 t is [] a id).snd) is'.permutations ++
      (map (fun x ↦ x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))

Tactic:
congr 2

Goal state after:
case cons.e_a.e_b
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (fun y ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) = fun a ↦
    map (fun x ↦ x ++ ts) (permutationsAux2 t is [] a id).snd
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
· exact
      ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
        (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))

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

Goal state before:
pp: case mem
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
z : A
hz : z ∈ s
⊢ p a z ha ⋯

Tactic:
induction ha using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h

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

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length + 1 < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
Nat.succ_lt_succ_iff

Goal state after:
case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y ↦ (permutationsAux2 t [] [] y id).snd) ts.permutations' ++
      flatMap (fun x ↦ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
refine (flatMap_append_perm _ _ _).trans ?_

Goal state after:
case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun x ↦ (permutationsAux2 t [] [] x id).snd ++ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prodMap]; exact Nat.dvd_lcm_left _ _

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : StarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S

Tactic:
cases S

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

Tactic:
cases S

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }.toStarSubalgebra
        h1).toNonUnitalStarSubalgebra =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (l.rotate (l.length - (l.reverse.length - 1) % l.length)).reverse[l.length - 1 - k] = (l.rotate 1)[k]

Tactic:
length_reverse,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (l.rotate (l.length - (l.length - 1) % l.length)).reverse[l.length - 1 - k] = (l.rotate 1)[k]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

Tactic:
ext; simp [stabilizerEquivStabilizer]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k

Tactic:
by rw [pow_mul', hn]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rw [isPrimePow_nat_iff]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
by
  rw [isPrimePow_nat_iff]
  constructor
  · rintro ⟨p, k, hp', hk', rfl⟩
    refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
    · calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)
  · rintro ⟨k, hk, hk', ⟨p, hp, rfl, hp'⟩⟩
    exact ⟨p, k, hp', hk', rfl⟩

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

Goal state before:
pp: case mp.cons
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ (L_hd :: L_tl).prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
| cons L_hd L_tl L_ih =>

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Tactic:
have hc' := hc n₁ n₂

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x

Tactic:
← ringEquivCongr_trans hab hbc

Goal state after:
a b c : ℕ
hab : a = b
hbc : b = c
x : ZMod a
⊢ (ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑(↑a).val

Tactic:
val

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range

Tactic:
rw [finite_iff_finite_and_finiteIndex f.ker, ← (QuotientGroup.quotientKerEquivRange f).finite_iff,
    finiteIndex_iff_finite_quotient]

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

Goal state before:
pp: p n : ℕ
_h : 0 ≤ ↑n
⊢ ↑(↑n).toNat = ↑↑n

Tactic:
simp only [Int.cast_natCast, Int.toNat_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #(Ico 1 (n + 1)) = n

Tactic:
card_Ico,

Goal state after:
n : ℕ
⊢ n + 1 - 1 = n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
⊢ m ∣ n → m = 1

Tactic:
hdvd

Goal state after:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
hdvd : m ∣ n
⊢ m = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).properDivisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range k)

Tactic:
by
  ext a
  simp [mem_properDivisors_prime_pow pp, eq_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
⊢ x ∈ z.divisors ↔ ∃ y ∈ z.natAbs.divisors, ↑y = x ∨ -↑y = x

Tactic:
by
    simp [← exists_or, ← and_or_left, divisors]

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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))

Tactic:
two_mul n,

Goal state after:
n : ℕ
⊢ 2 * ((n + n + 1).choose n * (n + 1)) = 2 * ((n + n + 1).choose n * (n + n + 1 - n))
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

Tactic:
by simp [add_self, eq_comm, ← sub_eq_zero]

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

Goal state before:
pp: case cons.w₂
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ (h : L ≠ []), L.getLast h ≠ 0

Tactic:
· intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂

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

Goal state before:
pp: case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2

Tactic:
intro d

Goal state after:
case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
⊢ d ∈ (b + 2).digits n → d < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ [n + 1].sum ≤ n + 1

Tactic:
List.sum_cons,

Goal state after:
case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ n + 1 + [].sum ≤ n + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1
hlt : n < b ^ (e + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

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

Goal state before:
pp: n : ℕ
⊢ n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

Tactic:
ext p
  simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + -b) = emultiplicity p b

Tactic:
emultiplicity_add_of_gt

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) = emultiplicity p b

α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (-b) < emultiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (a + -b) = multiplicity p b

Tactic:
hfin.neg.multiplicity_add_of_gt

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (-b) = multiplicity p b

α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (-b) < multiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
· simp [ha]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 := by
    apply factorization_eq_zero_of_not_dvd
    exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf y / (orderOf y).gcd m = orderOf y

Tactic:
h.gcd_eq_one,

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf y / 1 = orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i} ∪ {i ∈ Ico 1 n.succ | p ^ i ∣ k}) ≤ n

Tactic:
filter_union_right

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
by
  obtain _ | hprime := hR
  · simp only [one_pow, pow_one]
  · let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
    simp [hr]

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
⊢ #({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i} ∪ {i ∈ Ico 1 n.succ | p ^ i ∣ k}) ≤ n

Tactic:
filter_union_right

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
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})
⊢ #({x ∈ Ico 1 n.succ | p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k}) ≤ n
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b

Tactic:
by ext; simp [add_assoc]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n = ∏ p, ↑p ^ n.factorization ↑p

Tactic:
simpa using prod_primeFactors_pow_factorization hn

Goal state after:
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 ^ (Nat.card G).gcd n = (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:
h.gcd_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 = (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
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 ^ (Nat.card G).gcd n = (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:
h.gcd_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 = (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
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos.inr
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
exact
      (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
          ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div],
            (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2

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

Goal state before:
pp: case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
Nat.add_one_sub_one,

Goal state after:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ then 1 else 0) = 0