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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X

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

Tactic:
choose c hc using fun j ↦ hmj (i (nj j))

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
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)
⊢ n = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
⊢ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
x : A
⊢ ↑f x ∈ S.toNonUnitalSubalgebra
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
⊢ (lift f).range ≤ S

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra
x : Unitization R A
⊢ (lift f).toRingHom x ∈ S
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : (starLift f).range ≤ S
⊢ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : (starLift f).range ≤ S
x : A
⊢ ↑(NonUnitalAlgHomClass.toNonUnitalAlgHom f) x ∈ S.toNonUnitalStarSubalgebra
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
⊢ (starLift f).range ≤ S

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
x : Unitization R A
⊢ (↑(starLift f)).toRingHom x ∈ S
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1

Tactic:
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd

Tactic:
induction ys generalizing f f' with
  | nil => simp
  | cons ys_hd _ ys_ih =>
    simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
    rw [ys_ih]
    · refine ⟨?_, rfl⟩
      simp only [← map_cons, ← map_append]; apply H
    · intro a; apply H

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

Goal state before:
pp: 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

Tactic:
simp [ye]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R ⧸ I ^ (n + 1)
hx✝ : x ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
hx : ∃ x_1 ∈ I ^ n, (Quotient.mk (I ^ (n + 1))) x_1 = x
⊢ ∃ a, (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨x, hx✝⟩

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Goal state after:
case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
hx : (Quotient.mk (I ^ (n + 1))) y ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ ∃ a,
    (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a = ⟨(Quotient.mk (I ^ (n + 1))) y, hx⟩
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
rw [IsPeriodicPt, IsFixedPt, ← iterate_mul, ← Nat.mul_div_assoc _ (gcd_dvd_left _ _),
      mul_comm, Nat.mul_div_assoc _ (gcd_dvd_right _ _), mul_comm, 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).gcd n]^[minimalPeriod f x] x = x
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
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)

Tactic:
rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'

Goal state after:
case pos.refine_1.inl
α : 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
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

case pos.refine_1.inr
α : 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
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_2
α : 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
rw [iterate_zero_apply]

Goal state after:
case pos.refine_2
α : 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
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
⊢ ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n

Tactic:
simpa [Injective] using not_injective_infinite_finite (f^[·] x)

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
⊢ k < (permutations'Aux x s).length

Tactic:
simpa [Nat.lt_succ_iff] using hk.le

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (x :: y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d

Tactic:
unfold nextOr
    split_ifs with h'
    · grind
    apply nextOr_getLast_of_notMem_dropLast
    grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∈ l.dropLast
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

Tactic:
simp [next, nextOr_eq_getElem_idxOf_succ_of_mem_dropLast ha',
      Nat.mod_eq_of_lt <| succ_idxOf_lt_length_of_mem_dropLast ha']

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

Goal state before:
pp: case h
α : Type u_1
l : List α
h : l = [] ∨ ∃ a, l = [a]
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y

Tactic:
rcases h with (rfl | ⟨z, rfl⟩)

Goal state after:
case h.inl
α : Type u_1
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [] → x = y

case h.inr
α : Type u_1
z : α
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → x = y
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 : α
h : G
⊢ h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)

Tactic:
rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul,
    inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]

Goal state after:
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:
by
  ext; simp [stabilizerEquivStabilizer]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'

Tactic:
rw [heq_iff_eq] at hxy; subst x; simpa using isRotated_prev_eq h h₁ _

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ Chain r ↑(a :: l)

Tactic:
rw [Cycle.chain_coe_cons]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ IsChain r (a :: (l ++ [a]))
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 • x

Tactic:
rw [← smul_one_smul (G ⧸ H) g x, ← QuotientGroup.mk_one, Quotient.smul_coe,
    smul_eq_mul, mul_one]

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

Goal state before:
pp: case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
rw [mem_primeFactorsList_mul ha.ne' hb.ne', List.mem_union_iff]

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
⊢ K.index * H.relIndex K = H.index

Tactic:
simp_rw [relIndex, index, ← Nat.card_prod, Nat.card_congr <| quotientEquivProdOfLE h]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) * (K ⊓ L).relIndex L = (H ⊓ (K ⊓ L)).relIndex L

Tactic:
relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ (H ⊓ (K ⊓ L)).relIndex L = (H ⊓ (K ⊓ L)).relIndex L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: p n q : ℕ
h : n ≤ n + q
⊢ ↑p ^ n * ↑p ^ q = 0

Tactic:
← Nat.cast_pow

Goal state after:
p n q : ℕ
h : n ≤ n + q
⊢ ↑(p ^ n) * ↑p ^ q = 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
by
  constructor <;> intro h
  · rw [← h]; apply ZMod.val_lt
  · apply ZMod.val_mul_of_lt h

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ properDivisors 1 = ∅

Tactic:
by rw [properDivisors, Ico_self, filter_empty]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1

Tactic:
refine ⟨Nat.succ_le_iff.mpr <| one_mem_properDivisors_iff_one_lt.mp (by simp [h]), ?_⟩

Goal state after:
n : ℕ
h : n.properDivisors = {1}
⊢ ∀ m < n, m ∣ n → m = 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b k : ℕ
ih : ofDigits b (List.replicate k 0) = 0
⊢ ofDigits b (List.replicate (k + 1) 0) = 0

Tactic:
simp [List.replicate, ofDigits_cons, ih]

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

Goal state before:
pp: m k : ℕ
⊢ (Set.range fun n ↦ m * n + k) = {n | ↑n = ↑k ∧ k ≤ n}

Tactic:
ext n
  simp only [Set.mem_range, Set.mem_ofPred_eq]
  conv => enter [1, 1, y]; rw [add_comm, eq_comm]
  refine ⟨fun ⟨a, ha⟩ ↦ ⟨?_, le_iff_exists_add.mpr ⟨_, ha⟩⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  · simpa using congr_arg ((↑) : ℕ → ZMod m) ha
  · obtain ⟨a, ha⟩ := le_iff_exists_add.mp H₂
    simp only [ha, Nat.cast_add, add_eq_left, ZMod.natCast_eq_zero_iff] at H₁
    obtain ⟨b, rfl⟩ := H₁
    exact ⟨b, ha⟩

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

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

Tactic:
rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n.factorization.prod HPow.hPow * (f - n.factorization).prod HPow.hPow

Tactic:
prod_factorization_pow_eq_self hn

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
ha : FiniteMultiplicity p a
k : ℕ
⊢ multiplicity p (a ^ k) = k * multiplicity p a

Tactic:
by
  exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸
    ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p

Tactic:
refine (orderOf_dvd_lcm_mul h).trans (Nat.lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)

Goal state after:
case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p * orderOf x ∣ orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
by
  apply le_antisymm
  · have hdisj : Disjoint {i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}
        {i ∈ Ico 1 n.succ | p ^ i ∣ k} := by
      simp +contextual [Finset.disjoint_right, dvd_iff_mod_eq_zero, Nat.mod_lt _ (pow_pos hp.pos _)]
    rw [factorization_choose hp hkn (lt_succ_self _), factorization_eq_card_pow_dvd_of_lt hp
      hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt), log_pow hp.one_lt,
      ← card_union_of_disjoint hdisj, filter_union_right]
    have filter_le_Ico := (Ico 1 n.succ).card_filter_le
      fun x => p ^ x ≤ k % p ^ x + (p ^ n - k) % p ^ x ∨ p ^ x ∣ k
    rwa [card_Ico 1 n.succ] at filter_le_Ico
  · nth_rewrite 1 [← factorization_pow_self (n := n) hp]
    exact factorization_le_factorization_choose_add hkn hk0

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

Goal state before:
pp: a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
rcases em' p.Prime with (pp | pp)

Goal state after:
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
hab : a ∣ b
p : ℕ
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
rcases em' p.Prime with (pp | pp)

Goal state after:
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p n ! + emultiplicity p (n + 1) = ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1}))

Tactic:
emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb),

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + emultiplicity p (n + 1) =
    ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1}))
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (divX 1).coeff n✝ = coeff 0 n✝

Tactic:
simpa only [coeff_divX, coeff_zero] using! coeff_one

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
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS2 : S * S = S
pow_mem : ∀ a ∈ S, ∀ (n : ℕ), a ^ (n + 1) ∈ S
a : M
ha : a ∈ S
⊢ a ^ (orderOf a - succ 0 + succ 0) ∈ S

Tactic:
exact pow_mem a ha (orderOf a - 1)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
have := Fintype.ofFinite ι

Goal state after:
ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
this : Fintype ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
⊢ X ^ n ∣ f

Tactic:
by
    induction n with
    | zero => simp [pow_zero]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).leadingCoeff

Tactic:
leadingCoeff_monic_mul hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ p.leadingCoeff = (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)).leadingCoeff