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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Subalgebra.restrictScalars C (adjoin D S) =
    Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)

Tactic:
suffices
    Set.range (algebraMap D E) =
      Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E) by
    ext x
    change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
    rw [this]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : CommSemiring C
inst✝⁵ : CommSemiring D
inst✝⁴ : CommSemiring E
inst✝³ : Algebra C D
inst✝² : Algebra C E
inst✝¹ : Algebra D E
inst✝ : IsScalarTower C D E
S : Set E
⊢ Set.range ⇑(algebraMap D E) = Set.range ⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
n : ℕ
h✝ : Submodule.span R s ≤ degreeLE R ↑n
⊢ ∃ n, Submodule.span R s ≤ degreeLT R n

Tactic:
exact ⟨n + 1, by rwa [degreeLT_succ_eq_degreeLE]⟩

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

Goal state before:
pp: m k x : ℕ
hmk : m ∣ k
⊢ x ^ m - 1 ∣ x ^ k - 1

Tactic:
by
  simpa using pow_sub_pow_dvd_pow_sub_pow x 1 hmk

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inr.inr
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
← hf (yi * yj)

Goal state after:
case inr.inr
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ ∑ a ∈ y, f (yi * yj) a • a ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
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
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R (Set.range Subtype.val)) = Set.univ

Tactic:
Subtype.range_coe_subtype,

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R {x | x ∈ s}) = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R (Set.range Subtype.val)) = Set.univ

Tactic:
Subtype.range_coe_subtype,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R {x | x ∈ s}) = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
⊢ g.FiniteType

Tactic:
algebraize [f, g, g.comp f]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Algebra.FiniteType A C
⊢ g.FiniteType
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr.convert_2
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

Tactic:
by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
hpq : p - q * X ^ (k - q.natDegree) = 0
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s

case neg
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝² : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝¹ : 0 ≠ 1
this✝ : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
hq0 : q ≠ 0
h1 : p.degree = (q * X ^ (k - q.natDegree)).degree
h2 : p.leadingCoeff = (q * X ^ (k - q.natDegree)).leadingCoeff
this : (p - q * X ^ (k - q.natDegree)).degree < ↑p.natDegree
hpq : ¬p - q * X ^ (k - q.natDegree) = 0
⊢ p - q * X ^ (k - q.natDegree) ∈ Ideal.span ↑s
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
⊢ (Polynomial.C (F.coeff d) * d.prod fun n e ↦ f n ^ e).natDegree ≤ m * n

Tactic:
apply (Polynomial.natDegree_C_mul_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
⊢ (d.prod fun n e ↦ f n ^ e).natDegree ≤ m * n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1

Tactic:
by
  simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]

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

Goal state before:
pp: p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a

Tactic:
refine ⟨?_, by rintro rfl; rfl⟩
  rintro ⟨j, rfl⟩
  rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
  · exact mul_one _
  · exact (a1 rfl).elim

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

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y

Tactic:
by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Tactic:
apply h.minimalPeriod_of_comp_dvd_mul.antisymm
  suffices ∀ {f g : α → α},
      Commute f g →
        Coprime (minimalPeriod f x) (minimalPeriod g x) →
          minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
    hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
  intro f g h hco
  refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
  · exact (isPeriodicPt_minimalPeriod _ _).const_mul _
  · exact (isPeriodicPt_minimalPeriod _ _).mul_const _

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

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

Tactic:
rw [minimalPeriod_prodMap]

Goal state after:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

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

Tactic:
rw [minimalPeriod_prodMap]

Goal state after:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.length - 1 + 1 = l.length

Tactic:
grind [length_pos_iff]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + 1 + ([].length - 1)) % [].length] = [][n]

Tactic:
simp at hn

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
h : [].Nodup
hn : n < [].length
hx : [][n] ∈ []
⊢ [][(n + ([].length - 1) + 1) % [].length] = [][n]

Tactic:
simp at hn

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

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ s.reverse.Subsingleton ↔ s.Subsingleton

Tactic:
by
  simp [length_subsingleton_iff]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) = stabilizer G (g • a)

Tactic:
stabilizer_smul_eq_stabilizer_map_conj g a,

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
g h k : G
a b c : α
hg : b = g • a
⊢ Subgroup.map (↑(MulAut.conj g)) (stabilizer G a) =
    Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : ((c :: s ++ [a]).rotate 0).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rotate_zero,

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: s ++ [a]).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ IsChain r [a, a] ↔ r a a

Tactic:
List.isChain_pair

Goal state after:
α : Type u_1
r : α → α → Prop
a : α
⊢ r a a ↔ r a 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
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₁ : X
⊢ ∀ (b : X), (orbitRel (↥H) X) y₁ b → ↑⋯.choose = ↑⋯.choose

Tactic:
y₂

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
q : orbitRel.Quotient (↥H) X
y₁ y₂ : X
⊢ (orbitRel (↥H) X) y₁ y₂ → ↑⋯.choose = ↑⋯.choose
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Tactic:
refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)
    rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
    exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

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

Goal state before:
pp: n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList <+ (n * k).primeFactorsList

Tactic:
rcases n with - | hn

Goal state after:
case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList
Module: Mathlib.Data.Nat.PrimeFin

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

Tactic:
cases k

Goal state after:
case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors

case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors
Module: Mathlib.Data.Nat.Factors

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

Tactic:
constructor
    · rw [List.subperm_iff]
      rintro ⟨u, hu1, hu2⟩
      rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
      exact hu2.prod_dvd_prod
    · 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 K : Subgroup G
⊢ H.relIndex K = 2 ↔ ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H

Tactic:
rw [Subgroup.relIndex, Subgroup.index_eq_two_iff_exists_notMem_and']

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (∃ a ∉ H.subgroupOf K, ∀ (b : ↥K), a * b ∈ H.subgroupOf K ∨ b ∈ H.subgroupOf K) ↔
    ∃ a ∈ K, a ∉ H ∧ ∀ b ∈ K, a * b ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

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

Tactic:
by
  rw [mul_mem_iff_of_index_two h]

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

Goal state before:
pp: a n : ℕ
n0 : n ≠ 0
⊢ addOrderOf ↑a = n / n.gcd a

Tactic:
by
  rcases a with - | a
  · simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]
  rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]

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

Goal state before:
pp: p m n : ℕ
h : n ≤ m
⊢ ↑p ^ m = 0

Tactic:
by
  obtain ⟨q, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [pow_add, ← Nat.cast_pow]
  simp

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).relIndex L ≤ H.relIndex L * K.relIndex L

Tactic:
by_cases h : H.relIndex L = 0
  · simp [relIndex_eq_zero_of_le_left inf_le_left h]
  rw [← inf_relIndex_right, inf_assoc, ← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right,
    inf_relIndex_right, inf_relIndex_right]
  grw [relIndex_le_of_le_right inf_le_right h]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a * ↑↑b = ↑↑(a * b)

Tactic:
rw [← Nat.cast_mul, Fin.val_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a * ↑b - ↑a * ↑b % (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:

Tactic:
_ = a * Int.sign a := rfl
      _ = a.natAbs := by rw [Int.mul_sign_self]
      _ = a.natAbs.gcd 0 := by rw [Nat.gcd_zero_right]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Tactic:
· rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_ge ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun

Tactic:
intro x; rfl

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

Goal state before:
pp: case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun

Tactic:
intro x; rfl

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

Goal state before:
pp: hn : 1 < 0
x✝ : ZMod 0
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
simp at hn

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

Goal state before:
pp: hn : 1 < 1
x✝ : ZMod 1
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
simp at hn

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

Goal state before:
pp: n k : ℕ
⊢ (n + k).choose k ≤ (n + 1) ^ k

Tactic:
choose_eq_asc_factorial_div_factorial

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k / k ! ≤ (n + 1) ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.zero
k : ℕ
lt : ¬0 + 1 < k
⊢ (0 + 1).choose k ≤ 2 ^ 0

Tactic:
cases k

Goal state after:
case neg.zero.zero
lt : ¬0 + 1 < 0
⊢ (0 + 1).choose 0 ≤ 2 ^ 0

case neg.zero.succ
n✝ : ℕ
lt : ¬0 + 1 < n✝ + 1
⊢ (0 + 1).choose (n✝ + 1) ≤ 2 ^ 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0

Tactic:
cases k

Goal state after:
case inl.zero
⊢ choose 0 0 ≤ 2 ^ 0

case inl.succ
n✝ : ℕ
⊢ choose 0 (n✝ + 1) ≤ 2 ^ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
ih : ofDigits 1 tail✝ = tail✝.sum
⊢ ofDigits 1 (head✝ :: tail✝) = (head✝ :: tail✝).sum

Tactic:
simp [ofDigits, List.sum_cons, ih]

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

Goal state before:
pp: case inr
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
⊢ p ^ k ∣ p ^ a

Tactic:
exact Nat.pow_dvd_pow p hle

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
    rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
    refine Nat.succ_le_of_lt (log_pos hb ?_)
    contrapose! h
    exact div_eq_of_lt h

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

Goal state before:
pp: case neg
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : ¬b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
· exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

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

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
| succ p =>

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : ↑k ≤ emultiplicity a b
⊢ a ^ k ∣ b

Tactic:
cases k

Goal state after:
case zero
α : Type u_1
inst✝ : Monoid α
a b : α
hk : ↑0 ≤ emultiplicity a b
⊢ a ^ 0 ∣ b

case succ
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
hk : ↑(n✝ + 1) ≤ emultiplicity a b
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) {L | L.length = l ∧ ∀ x ∈ L, x < b}

Tactic:
convert! bijOn_digitsAppend hb l

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ↑(Finset.range (b ^ l)) = {n | n < b ^ l}
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
refine ⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩
  · rw [← prod_factorization_pow_eq_self hn, ← prod_factorization_pow_eq_self hd]
    exact prod_dvd_prod_of_subset_of_dvd (support_mono hdn) fun a _ ↦ pow_dvd_pow a (hdn a)
  · subst h
    rw [factorization_mul hd <| right_ne_zero_of_mul hn]
    apply self_le_add_right

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

Goal state before:
pp: n k : ℕ
⊢ (n ^ k).factorization = k • n.factorization

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    rcases eq_or_ne n 0 with (rfl | hn)
    · simp
    rw [Nat.pow_succ, mul_comm, factorization_mul hn (pow_ne_zero _ hn), ih,
      add_smul, one_smul, add_comm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
x : G
⊢ IsOfFinOrder x ↔ IsUnit x

Tactic:
use IsOfFinOrder.isUnit

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
x : G
⊢ IsUnit x → IsOfFinOrder x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
rwa [zpow_add, zpow_mul, zpow_mul, zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key

Goal state after: