mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case e_a.e_a
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)

Tactic:
mem_range

Goal state after:
case e_a.e_a
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j < m
⊢ n - 1 - j = n - m + (m - 1 - j)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun x ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
⊢ ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

Tactic:
refine ⟨a, has, fun p hp => ?_⟩

Goal state after:
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
hs : s.Nonempty
a : R[X]
has : a ∈ s
hmax : ∀ ⦃j : R[X]⦄, (fun x ↦ x ∈ s) j → a.degree ≤ j.degree → j.degree ≤ a.degree
p : R[X]
hp : p ∈ Submodule.span R s
⊢ p.degree ≤ a.degree
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
rw [leadingCoeff, Submodule.mem_iSup_of_directed]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

case H
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun n ↦ I.leadingCoeffNth n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit r

Tactic:
← constantCoeff_C _ r

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.42
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
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
val✝ : Fintype ι
⊢ adjoin S (MvPolynomial.X '' Set.univ) = ⊤

Tactic:
Set.image_univ

Goal state after:
case intro
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
val✝ : Fintype ι
⊢ adjoin S (Set.range MvPolynomial.X) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case intro
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
val✝ : Fintype ι
⊢ adjoin S (FreeAlgebra.ι S '' Set.univ) = ⊤

Tactic:
Set.image_univ

Goal state after:
case intro
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
val✝ : Fintype ι
⊢ adjoin S (Set.range (FreeAlgebra.ι S)) = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
f : FreeAlgebra R ↥s →ₐ[R] A
hsur : Surjective ⇑f
⊢ ∃ ι x f, Surjective ⇑f

Tactic:
use { x : A // x ∈ s }, inferInstance, f

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inl
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✝ x : ↥N
hx : x = n
⊢ i x ∈ M'

pp: case refine_1.mem.inr
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 : Fin k
⊢ i (nj j) ∈ M'

Tactic:
· rw [hx, ← hb, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j _ ↦ ?_
        let b' : A := ⟨b j, Subring.subset_closure (by simp)⟩
        rw [show b j • mj j = b' • mj j from rfl]
        exact smul_mem _ _ (subset_span (by simp))

Goal state after:
case refine_1.mem.inr
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 : Fin k
⊢ i (nj j) ∈ M'
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I

Tactic:
by
  rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]

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

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

Tactic:
by
  refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
  rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
  exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

Goal state after:
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
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n

Tactic:
by
  have hpd : p ^ (k + l) * p ∣ m * n := by
      let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
      rwa [pow_succ'] at hpmn'
  have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
  have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
  have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
  have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l :=
    (Prime.dvd_mul p_prime).1 hpd4
  suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ, _root_.pow_succ]
  exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h

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

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
⊢ ∀ (r : R ⧸ p) (x : A ⧸ P), (quotientMap P (algebraMap R A) h) r * x = x * (quotientMap P (algebraMap R A) h) r

Tactic:
rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.commutes _ _)

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

Goal state before:
pp: 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 : List α
ha : a ~ m.toList
b : List α
hb : b ~ n.toList
hab : a = b
⊢ m = n

Tactic:
rw [hab] at ha

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 b : List α
ha : b ~ m.toList
hb : b ~ n.toList
hab : a = b
⊢ m = n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt f^[n + m] x

Tactic:
iterate_add

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt f^[n + m] x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Tactic:
iterate_add

Goal state after:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
⊢ (∃ is'_1 x, is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

Tactic:
subst is'

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ period m a ∣ n

Tactic:
rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = sInf {n | n > 0 ∧ IsPeriodicPt f n x}

Tactic:
by
  dsimp +instances [minimalPeriod, periodicPts, sInf]
  grind

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

Goal state before:
pp: 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✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
⊢ x ∈ φ.range → x ∈ map φ ⊤

Tactic:
rintro ⟨a, ha⟩; exact ⟨a, by simp, ha⟩

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

Goal state before:
pp: 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✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
⊢ x ∈ map φ ⊤ → x ∈ φ.range

Tactic:
rintro ⟨a, -, ha⟩

Goal state after:
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✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ↑↑φ a = x
⊢ x ∈ φ.range
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right.inr.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (as.insertIdx n x)[m] = x
hx' : (bs.insertIdx m x)[n] = x
ht : n = m
⊢ False

Tactic:
simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')

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

Goal state before:
pp: α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' l)

Tactic:
refine List.recOn l ?_ ?_

Goal state after:
case refine_1
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' [])

case refine_2
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), motive (Quotient.mk'' tail) → motive (Quotient.mk'' (head :: tail))
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsCancelSMul G α ↔ ∀ (a : α), stabilizer G a = ⊥

Tactic:
simp [isCancelSMul_iff_eq_one_of_smul_eq, Subgroup.eq_bot_iff_forall, forall_comm (α := G)]

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 α
a : α
⊢ stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(stabilizer G a)

Tactic:
by
  ext; simp [stabilizerEquivStabilizer_apply]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Tactic:
constructor
  · intro hyp g hg
    apply Eq.subset
    rw [← mem_stabilizer_iff]
    exact hyp hg
  · intro hyp g hg
    rw [mem_stabilizer_iff]
    apply subset_antisymm (hyp g hg)
    intro x hx
    use g⁻¹ • x
    constructor
    · apply hyp g⁻¹ (inv_mem hg)
      simp only [Set.smul_mem_smul_set_iff, hx]
    · simp only [smul_inv_smul]

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

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList

Tactic:
rintro ⟨c, rfl⟩
      rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
      rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]
      exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
by
  by_cases ha : a ∈ H; · simp only [ha, true_iff, mul_mem_cancel_left ha]
  by_cases hb : b ∈ H; · simp only [hb, iff_true, mul_mem_cancel_right hb]
  simp only [ha, hb, iff_true]
  rcases index_eq_two_iff.1 h with ⟨c, hc⟩
  refine (hc _).or.resolve_left ?_
  rwa [mul_assoc, mul_mem_cancel_right ((hc _).or.resolve_right hb)]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0

Tactic:
exact relIndex_ne_zero_trans hH hK

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
pointwise_smul_def K,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (h • J).relIndex (map ((MulDistribMulAction.toMonoidEnd H G) h) K) = J.relIndex K
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
pointwise_smul_def K,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (h • J).relIndex (map ((DistribMulAction.toAddMonoidEnd H G) h) K) = J.relIndex K
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
rw [ZMod.intCast_eq_intCast_iff]

Goal state after:
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}

Tactic:
← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),

Goal state after:
n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ some (a, n / a) = some d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ some (b, n / b) = some ha
⊢ d.1 < ha.1

Tactic:
Option.some.injEq

Goal state after:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h : a * (n / a) = n ∧ (a, n / a) = d
ha : ℕ × ℕ
h' : b * (n / b) = n ∧ (b, n / b) = ha
⊢ d.1 < ha.1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors

Tactic:
rw [mul_ne_zero_iff] at hn

Goal state after:
case refine_2
m k : ℕ
hk : k > 1
hn : m ≠ 0 ∧ k ≠ 0
⊢ m ∈ (m * k).properDivisors
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
h : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
rcases n with (_ | _ | k)
  · exact (Nat.not_odd_zero h).elim
  · simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]
  rw [← Nat.not_even_iff_odd] at h
  rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
  · have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
    simp only [h, if_false] at this
    exact zero_lt_one.trans this
  · simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]
  · exact geom_sum_pos' hx k.succ.succ_ne_zero

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n) ≤
    ∑ i ∈ range n, a / b ^ i + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
gcongr with i hi

Goal state after:
case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val

Tactic:
rintro (rfl | h)

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0

case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)

Tactic:
refine Nat.le_mul_of_pos_left _ zero_lt_two

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

Goal state before:
pp: case zero
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ 0 < n
⊢ (a ^ 0).val = a.val ^ 0

Tactic:
simp [ZMod.val_one]

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

Goal state before:
pp: case zero
n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ 0).val ≤ a.val ^ 0

Tactic:
simp [ZMod.val_one]

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b

Tactic:
induction l

Goal state after:
case nil
b : ℕ
⊢ ofDigits b [] % b = [].head! % b

case cons
b head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofDigits b tail✝ % b = tail✝.head! % b
⊢ ofDigits b (head✝ :: tail✝) % b = (head✝ :: tail✝).head! % b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
⊢ False

Tactic:
have := h.count_le p

Goal state after:
case a
n p : ℕ
hn0 : n > 0
pp : Prime p
h : replicate (count p n.primeFactorsList + 1) p <+~ n.primeFactorsList
this : count p (replicate (count p n.primeFactorsList + 1) p) ≤ count p n.primeFactorsList
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity ↑a ↑b.natAbs

Tactic:
rw [Int.natCast_emultiplicity]

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
rw [← add_tsub_cancel_of_le hf, Finsupp.prod_add_index' (by simp) Nat.pow_add,
    prod_factorization_pow_eq_self hn]
  apply n.dvd_mul_right

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b