mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ : ↥M'
x : M
hx : x ∈ M'
a : ↥N'
ha : ((↑↥A f).domRestrict N') a = x
⊢ ∃ a, ((↑↥A f).restrict ⋯) a = ⟨x, hx⟩

Tactic:
exact ⟨a, Subtype.val_injective ha⟩

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b * n + c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
rw [add_comm, modEq_add_mul_modulus_iff]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑a = ↑b ↔ a ≡ b [MOD p]

Tactic:
eq_comm,

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsRightCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a ≡ b [MOD p])
hle : ¬a ≤ b
⊢ ↑b = ↑a ↔ a ≡ b [MOD p]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℤ
⊢ ↑b = ↑a ↔ a ≡ b [ZMOD ↑p]
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card { a // a ≠ 0 } = Nat.card α - 1

Tactic:
eq_comm,

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card α - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card { a // a = 0 } + Nat.card { a // ¬a = 0 } - 1 = Nat.card { a // a ≠ 0 }

Tactic:
Nat.card_unique,

Goal state after:
case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ 1 + Nat.card { a // ¬a = 0 } - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1

Tactic:
rw [Nat.card_units, tsub_add_cancel_of_le Nat.card_pos]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
⊢ ↑n = 0 ↔ 2 ∣ n

Tactic:
by
    obtain hn | hn := Nat.even_or_odd n
    · simp_rw [hn.two_dvd, iff_true]
      exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂
    · simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : -1 = 1
⊢ ringChar R = 2

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : 1 = -1
⊢ ringChar R = 2
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p ^ (k + l).succ ∣ m * n := hpmn
⊢ p ^ (k + l) * p ∣ m * n

Tactic:
pow_succ'

Goal state after:
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p * p ^ (k + l) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup

Tactic:
rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup

Goal state after:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup
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✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
x✝¹ x✝ : StarSubalgebra R A
⊢ x✝¹.toNonUnitalStarSubalgebra = x✝.toNonUnitalStarSubalgebra → x✝¹ = x✝

Tactic:
by simp [SetLike.ext_iff]

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

Goal state before:
pp: case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[1] (f^[n - 1] x) = x

Tactic:
rw [← iterate_add_apply, Nat.add_sub_cancel' (by lia)]

Goal state after:
case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[n] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n m : ℕ
hm : m > 0
hx : IsPeriodicPt f m x
⊢ f^[n] x ∈ periodicPts f

Tactic:
exact ⟨m, hm, hx.apply_iterate n⟩

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:
| mem z hz =>

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)

Tactic:
rintro ⟨hr, H⟩ n hn

Goal state after:
case pos.refine_1
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ a = g ^ (n + 1) • a ↔ ↑(period g a) ∣ -↑(n + 1)

Tactic:
eq_comm,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

Tactic:
← Nat.card_prod,

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card (↥s × ↑(QuotientGroup.mk '' t))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ (hd :: tl).prev x h ∈ hd :: tl

Tactic:
induction tl generalizing hd with
  | nil => simp
  | cons hd' tl hl =>
    by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)

Goal state after:
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.reverse.prev l[k] ⋯ = (pmap l.next l ⋯)[k]

Tactic:
simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]

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.reverse.prev l.reverse[l.length - 1 - k] ⋯ = (l.rotate 1)[k]
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ (n ^ k).minFac = n.minFac

Tactic:
by
  rcases eq_or_ne n 1 with (rfl | hn)
  · simp
  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff_left hk).1 hk')
  apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
  apply
    minFac_le_of_dvd (minFac_prime hnk).two_le
      ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))

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

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

Tactic:
intro h
    induction L with
    | nil =>
      rw [prod_nil] at h
      exact absurd h pp.not_dvd_one
    | cons L_hd L_tl L_ih =>
      rw [prod_cons] at h
      rcases pp.dvd_or_dvd h with hd | hd
      · exact ⟨L_hd, mem_cons_self, hd⟩
      · obtain ⟨x, hx1, hx2⟩ := L_ih hd
        exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ unop ↑b * ((unop ↑b)⁻¹ * (c⁻¹ * x✝¹)) ∈ H

Tactic:
mul_inv_cancel_left

Goal state after:
G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ c⁻¹ * x✝¹ ∈ H
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H

Tactic:
rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]

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

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ q = g ^ minimalPeriod (fun x ↦ g • x) q • q

Tactic:
eq_comm,

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ g ^ minimalPeriod (fun x ↦ g • x) q • q = q
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = (g • ↑1) • x

Tactic:
Quotient.smul_coe,

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = ↑(g • 1) • x
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
g : G ⧸ stabilizer G x
g1 g2 : G
H : (leftRel (stabilizer G x)) g1 g2
⊢ (g1 * (g1⁻¹ * g2)) • x = g2 • x

Tactic:
mul_inv_cancel_left

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
g : G ⧸ stabilizer G x
g1 g2 : G
H : (leftRel (stabilizer G x)) g1 g2
⊢ g2 • x = g2 • x
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose = g

Tactic:
eq_comm,

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ g = ⋯.choose
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 G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]

Goal state after:
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 (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ Nat.card (G ⧸ K) * Nat.card (↥K ⧸ H.subgroupOf K) = Nat.card (G ⧸ H)

Tactic:
← Nat.card_prod,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ Nat.card ((G ⧸ K) × ↥K ⧸ H.subgroupOf K) = Nat.card (G ⧸ H)
Module: Mathlib.GroupTheory.Index

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

Tactic:
by simpa using mul_mem (inv_mem h'.2) h'.1

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index * Nat.card ↥H = Nat.card G

Tactic:
by
  rw [mul_comm, card_mul_index]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ a.val < n

Tactic:
by
  cases n
  · cases NeZero.ne 0 rfl
  exact Fin.is_lt a

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index ≠ 0 ↔ Finite (G ⧸ H)

Tactic:
simp [index_eq_zero_iff_infinite]

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
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
eq_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ℕ
h : a = b
x : ZMod a
⊢ ((ringEquivCongr h) x).val = x.val

Tactic:
by
  subst h
  cases a <;> rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬K.index = H.relIndex K * K.index

Tactic:
eq_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
h : H < K
inst✝ : H.FiniteIndex
h0 : K.index ≠ 0
⊢ ¬H.relIndex K * K.index = K.index
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x✝ : n.divisors.Nonempty
hn : n = 0
m : ℕ
hm : m ∈ n.divisors
⊢ False

Tactic:
by simp [hn] at hm

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ) = ↑(a.val.gcd n.succ)

Tactic:
rw [← Nat.gcd_eq_gcd_ab a.val n.succ]

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
    split_ifs at this
    · exact this.ne
    · exact (zero_lt_one.trans this).ne'

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
⊢ 0 < ∑ i ∈ range n, x ^ i ∨ 0 = ∑ i ∈ range n, x ^ i ↔ ¬(Even n ∧ x + 1 < 0)

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i ∨ ∑ i ∈ range n, x ^ i = 0 ↔ ¬(Even n ∧ x + 1 < 0)
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) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
eq_comm,

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 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)

Tactic:
by
  rcases n with - | n
  · rw [Ico_eq_empty_of_le (by lia), sum_empty]
    exact Nat.zero_le _
  rw [← add_le_add_iff_left a]
  calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

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

Goal state before:
pp: case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

Tactic:
clear IH

Goal state after:
case h.inl
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) = 4 * 4 ^ n

Tactic:
pow_succ'

Goal state after:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * 4 ^ n = 4 * 4 ^ n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ ?m.35 ≠ 0

Tactic:
by rintro (rfl : n = 0); simp at h

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

Goal state before:
pp: case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b ^ (tl.length + 1) * ofDigits b l2

Tactic:
pow_succ'

Goal state after:
case cons
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b k : ℕ
l : List ℕ
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l

Tactic:
rw [ofDigits_append]

Goal state after:
b k : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d

Tactic:
rw [ofDigits_append]

Goal state after:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
by
  simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

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

Goal state before:
pp: m k n : ℕ
⊢ (∃ y, n = k + m * y) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Goal state after:
case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k

case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₂ : k ≤ n
b : ℕ
ha : n = k + m * b
⊢ ∃ y, n = k + m * y

Tactic:
exact ⟨b, ha⟩

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

Goal state before:
pp: case neg
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
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ (d :: L).getLast ⋯ ∈ L

Tactic:
List.getLast_cons h'

Goal state after:
case neg
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
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ L.getLast h' ∈ L
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * (p ^ padicValNat p n * n.divMaxPow p) = p ^ k * n

Tactic:
pow_padicValNat_mul_divMaxPow

Goal state after:
case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n = p ^ k * n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ ofDigits b L =
    (List.map
        (fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        (L.zip (List.range' 0 L.length))).sum

Tactic:
List.map_zip_eq_zipWith,

Goal state after:
b : ℕ
L : List ℕ
⊢ ofDigits b L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range' 0 L.length)).sum
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
cases m
    · cases hm rfl
    · simp

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

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

Tactic:
by
  rw [digits_def' hb (by positivity)]
  simp [mul_div_right m (by positivity)]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≤ multiplicity a b
⊢ ↑n ≤ emultiplicity a b

Tactic:
by
  exact_mod_cast (WithTop.coe_mono h).trans multiplicity_le_emultiplicity

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p n) = emultiplicity p n

Tactic:
eq_comm,

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p n = ↑(padicValNat p n)