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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ OrzechProperty R

Tactic:
refine ⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩

Goal state after:
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
⊢ Function.Injective ⇑f
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 : ↥N
j j' : Fin k
x✝ : j' ∈ Finset.univ
⊢ c j j' ∈ Set.range b ∪ Set.range (Function.uncurry c)

Tactic:
simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.smul
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✝ : ↥N
a : ↥A
x : ↥N
hx✝ : x ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A i) x ∈ M'
⊢ (↑↥A i) (a • x) ∈ M'

Tactic:
| smul a x _ hx =>

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ ((fun n e ↦ f n ^ e) i (d i)).natDegree ≤ d i * n

Tactic:
apply Polynomial.natDegree_pow_le.trans

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ d i * (f i).natDegree ≤ d i * n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_2.smul
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✝ : ↥N
a : ↥A
x : ↥N
hx✝ : x ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A f) x ∈ M'
⊢ (↑↥A f) (a • x) ∈ M'

Tactic:
| smul a x _ hx =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3.smul
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
a : ↥A
x : M
hx✝ : x ∈ span (↥A) (Set.range mj)
hx : x ∈ ((↑↥A f).domRestrict N').range
⊢ a • x ∈ ((↑↥A f).domRestrict N').range

Tactic:
| smul a x _ hx =>

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

Goal state before:
pp: case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m.gcd c / (↑(m.gcd c)).natAbs = 1

Tactic:
natAbs_natCast,

Goal state after:
case refine_2
m a b c : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := m.gcd c
⊢ m.gcd c / m.gcd c = 1
Module: Mathlib.Data.Int.ModEq

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

Tactic:
rw [add_comm, add_mul_modulus_modEq_iff]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

pp: case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Tactic:
· exact false_of_nontrivial_of_char_one (R := R)

Goal state after:
case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card α = card αˣ + 1

Tactic:
by
  rw [Fintype.card_units, tsub_add_cancel_of_le Fintype.card_pos]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ↑0 = if Even 0 then 0 else 1

Tactic:
aesop (add simp [one_add_one_eq_two])

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n✝ : ℕ
a✝ : ↑n✝ = if Even n✝ then 0 else 1
⊢ ↑(n✝ + 1) = if Even (n✝ + 1) then 0 else 1

Tactic:
aesop (add simp [one_add_one_eq_two])

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

Goal state before:
pp: p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬2 = 1

Tactic:
by decide

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

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬m.Coprime n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
intro h

Goal state after:
case mp
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n

Tactic:
intro h

Goal state after:
case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬m.Coprime n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) → I = ⊥

Tactic:
intro h

Goal state after:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
h : Bijective ⇑(mk I)
⊢ I = ⊥
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf).symm (f a) = (Quotient.mk (ker f)) a

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hf).injective

Goal state after:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf) ((quotientKerAlgEquivOfSurjective hf).symm (f a)) =
    (quotientKerAlgEquivOfSurjective hf) ((Quotient.mk (ker f)) a)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ((quotientMap I f H).comp (Quotient.mk J)) x = ((Quotient.mk I).comp f) x

Tactic:
by simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
⊢ ¬m = n
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
h : ¬m = n
⊢ ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2.mp
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) → l.Nodup

Tactic:
intro h

Goal state after:
case refine_2.mp
α : Type u_1
inst✝ : Fintype α
l : List α
h : ∃ a, a.val = ↑l
⊢ l.Nodup
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ l.Nodup → ∃ a, a.val = ↑l

Tactic:
intro h

Goal state after:
case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ ∃ a, a.val = ↑l
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
hd : d ∈ xs
⊢ xs.nextOr x d ∈ xs

Tactic:
by
  revert hd
  suffices ∀ xs' : List α, (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs' by
    exact this xs fun _ => id
  intro xs' hxs' hd
  induction xs with
  | nil => exact hd
  | cons y ys ih => ?_
  rcases ys with - | ⟨z, zs⟩
  · exact hd
  rw [nextOr]
  split_ifs with h
  · exact hxs' _ (mem_cons_of_mem _ mem_cons_self)
  · exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)

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

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
h : p ∣ L.prod
⊢ ∃ a, a ∈ L ∧ p ∣ a
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
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : (rightRel H) g₂ g₁
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧

Tactic:
rw [rightRel_eq] at r

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : g₁ * g₂⁻¹ ∈ H
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp
n : ℕ
⊢ n.primeFactorsList = [] → n = 0 ∨ n = 1

Tactic:
intro h

Goal state after:
case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactorsList = []

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = ∅ ↔ n = 0 ∨ n = 1

Tactic:
by
  constructor
  · contrapose!
    rintro hn
    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
    exact ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
  · rintro (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (f x) = Quotient.mk'' (f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄, Quotient.map' ⇑f ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ a₂ → Quotient.mk'' x = a₂

Tactic:
refine Quotient.ind' fun y => ?_

Goal state after:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (f x) = Quotient.mk'' (f y)
x y : G'
⊢ Quotient.map' ⇑f ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ (Quotient.mk'' y) → Quotient.mk'' x = Quotient.mk'' y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n a : ℕ
h : a < n
⊢ (↑a).val = a

Tactic:
rwa [val_natCast, Nat.mod_eq_of_lt]

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

Goal state before:
pp: case succ
n : ℕ
a b : Fin (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ cast a + cast b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _

Goal state after:
case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑↑(a + b) = if ↑(n + 1) ≤ ↑↑a + ↑↑b then cast a + cast b - ↑(n + 1) else cast a + cast b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
k : ZMod n
hk : k = 0
⊢ (k - 1).cast = ↑n - 1

Tactic:
rw [hk, zero_sub, ZMod.cast_neg_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Group M
inst✝¹ : Finite G
inst✝ : Finite M
f : G →* M
h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M
⊢ Nat.card M ≤ Nat.card (G ⧸ f.ker)

Tactic:
exact Nat.le_of_mul_le_mul_left (f.ker.card_mul_index ▸ Nat.mul_le_of_le_div _ _ _ h) Nat.card_pos

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : M
hx : x ∈ Set.range ⇑f
hy : y ∈ Set.range ⇑f
⊢ #{g | f g = x} = #{g | f g = y}

Tactic:
by
  rcases hx with ⟨x, rfl⟩
  rcases hy with ⟨y, rfl⟩
  rcases mul_left_surjective x y with ⟨y, rfl⟩
  conv_lhs =>
    rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
  congr 2 with g
  simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]
  let f' := MonoidHomClass.toMonoidHom f
  change f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
  rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]

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

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val → a.val * b.val < n

Tactic:
intro h

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ a.val * b.val < n → (a * b).val = a.val * b.val

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
intro h

Goal state after:
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ {1, p}.erase p = {1}

Tactic:
pair_comm,

Goal state after:
p : ℕ
pp : Prime p
⊢ {p, 1}.erase p = {1}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x → s = (n✝ + 1).properDivisors

Tactic:
intro h

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ s = (n✝ + 1).properDivisors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ ∀ (a : (ZMod 2)ˣ), a = 1

Tactic:
by decide

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

Goal state before:
pp: n✝ : ℕ
h : 1 < 0
⊢ ¬1 < 0

Tactic:
by decide

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

Goal state before:
pp: n✝ : ℕ
h : 1 < 1
⊢ ¬1 < 1

Tactic:
by decide

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

Goal state before:
pp: case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
h : AddSubgroup.zmultiples ↑n ≤ f.ker
⊢ f ↑n = 0
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
⊢ ∀ l ∈ L, l < b

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 l m
        apply w₁
        exact List.mem_cons_of_mem _ m

Goal state after:
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
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

Goal state after:
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
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
induction L with
  | nil => simp
  | cons d L ih =>
    dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

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 < m

Tactic:
exact Nat.div_lt_self (by grind) hp.1

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

Goal state before:
pp: case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

Tactic:
intro h

Goal state after:
case mp
b n : ℕ
h : b.digits n = []
⊢ n = 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih✝ :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)