mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
b : MvPolynomial σ S₁
hb : ∃ a, (map f) a = b
a : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + b

Tactic:
obtain ⟨b, rfl⟩ := hb

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Surjective ⇑f
a b : MvPolynomial σ R
⊢ ∃ a_1, (map f) a_1 = (map f) a + (map f) b
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ (rename Subtype.val) q = (rename (Subtype.val ∘ ⇑e.symm)) ((rename ⇑e) q)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∉ p.vars
⊢ i ∉ s.support

Tactic:
simp [mem_support_notMem_vars_zero h hi]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ cons 0 0 = 0

Tactic:
simp [cons_zero_eq_single_zero]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun i ↦ (f i).totalDegree)

Tactic:
exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ ((monomial n) a).trailingDegree

Tactic:
exact le_trailingDegree_monomial

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
simp [hx0, IH]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
natDegree_sub,

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q - p).natDegree ≤ n ↔ q.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect N f.eraseLead * reflect O g + reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g

pp: case neg.Cf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

pp: case neg.Nf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N

Tactic:
hcf

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g =
    reflect N f.eraseLead * reflect O g + reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g

case neg.Cf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #(C f.leadingCoeff * X ^ f.natDegree).support ≤ cf.succ

case neg.Nf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

case neg.Cf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

case neg.Nf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ (∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i) →
    ∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff i) = 0

Tactic:
· rintro ⟨m, h, rfl⟩
    exact ⟨some m, h⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
· rw [hpi]; simpa

Goal state after:
case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.coeff 0 = f.leadingCoeff

Tactic:
rw [coeff_reverse, revAt_le zero_le, tsub_zero, leadingCoeff]

Goal state after:
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 : R[X]
hp : p ∈ Submodule.span R s
p' : R[X]
hp' : p' ∈ s
hpp' : p.degree ≤ p'.degree
⊢ p.degree ≤ a.degree

Tactic:
exact hpp'.trans <| not_lt.1 <| not_lt_iff_le_imp_ge.2 <| hmax hp'

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ span R ↑t

Tactic:
rw [ht]

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Algebra.adjoin R ↑(Finset.image (⇑f) s) = Subalgebra.map f S

Tactic:
rw [Finset.coe_image, Algebra.adjoin_image, hs]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff →
        ∏ i ∈ insert a s, (f i).leadingCoeff ≤ ((insert a s).prod f).leadingCoeff

Tactic:
intro i s hi hs

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s✝ : Finset ι
f : ι → Ideal R[X]
i : ι
s : Finset ι
hi : i ∉ s
hs : ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
⊢ ∏ i ∈ insert i s, (f i).leadingCoeff ≤ ((insert i s).prod f).leadingCoeff
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocSemiring R
S : Subsemiring R
a✝ b✝ : Rᵐᵒᵖ
hx : a✝ ∈ S.op.carrier
hy : b✝ ∈ S.op.carrier
⊢ a✝ + b✝ ∈ S.op.carrier

Tactic:
simp_all [add_mem]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: ι : Sort u_1
R : Type u_2
inst✝ : NonAssocSemiring R
S : Subsemiring Rᵐᵒᵖ
a✝ b✝ : R
hx : a✝ ∈ S.unop.carrier
hy : b✝ ∈ S.unop.carrier
⊢ a✝ + b✝ ∈ S.unop.carrier

Tactic:
simp_all [add_mem]

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

Goal state before:
pp: 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
⊢ ↑p.natDegree = ↑q.natDegree + ↑(k - q.natDegree)

Tactic:
rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]

Goal state after:
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
⊢ q.natDegree ≤ k
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]

Tactic:
let d := gcd m c

Goal state after:
m a b c : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := m.gcd c
⊢ a ≡ b [ZMOD m / ↑(m.gcd c)]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case prime.prime
R : Type u_1
inst✝³ : AddMonoidWithOne R
S : Type u_2
inst✝² : Semiring S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
hp : Nat.Prime p
hchar✝¹ : CharP R p
hprime✝ : Nat.Prime p
hchar✝ : CharP S p
⊢ ExpChar (R × S) p

Tactic:
· have := Prod.charP R S p; exact .prime hp

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise (IsCoprime on I)
r : R
⊢ ∃ r_1, ∀ (i : ι), (Quotient.mk (I i)) r_1 = (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) r) i

Tactic:
exact ⟨r, fun i ↦ rfl⟩

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:
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: case mp
m n : ℕ
⊢ ¬m.Coprime n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
intro h
    exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩

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

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra R A
inst✝⁸ : StarModule R A
inst✝⁷ : Semiring B
inst✝⁶ : StarRing B
inst✝⁵ : Algebra R B
inst✝⁴ : StarModule R B
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
S : StarSubalgebra R C
g : B →⋆ₐ[R] C
f : A →⋆ₐ[R] B
⊢ ↑(comap f (comap g S)) = ↑(comap (g.comp f) S)

Tactic:
by exact Set.preimage_preimage

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))

Tactic:
intro
    simp [Submodule.mem_smul_top_iff, pow_succ']

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : NonUnitalStarSubalgebra R A
⊢ Subalgebra.toSubmodule (adjoin R ↑s).toSubalgebra = R ∙ 1 ⊔ s.toSubmodule

Tactic:
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union,
    ← NonUnitalStarAlgebra.adjoin_eq_span, NonUnitalStarAlgebra.adjoin_eq]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ ∃ x_1, Duplicate x_1 ([x, x] ++ l).permutations

Tactic:
use x :: x :: l

Goal state after:
case h
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh✝ : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
yh : Quotient.mk'' y = Quotient.mk'' a✝
z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : Quotient.mk'' z = Quotient.mk'' a✝
⊢ ∃ g, g • ⟨y, yh✝⟩ = ⟨z, zh✝⟩

Tactic:
Quotient.eq''

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh✝ : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
yh : (orbitRel G α) y a✝
z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : (orbitRel G α) z a✝
⊢ ∃ g, g • ⟨y, yh✝⟩ = ⟨z, zh✝⟩
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rintro ⟨k, hkle, hk_pos, heq⟩

Goal state after:
case inr.mpr
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors

Tactic:
simp only [subset_iff, mem_primeFactors, and_imp]

Goal state after:
m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ ∀ ⦃x : ℕ⦄, Prime x → x ∣ m → m ≠ 0 → Prime x ∧ x ∣ n ∧ n ≠ 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
n2 : 2 < n
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
  · contradiction
  · contradiction
  · simp [Nat.pow_succ, mul_assoc]
  · exact Or.inr ⟨p, hp, hdvd, hodd⟩

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 y : G'
⊢ Quotient.map' ⇑f ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ (Quotient.mk'' y) → Quotient.mk'' x = Quotient.mk'' y

Tactic:
exact (key x y).mpr

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
hf : Injective ⇑f
⊢ (map f H).relIndex (map f K) = H.relIndex K

Tactic:
← Subgroup.relIndex_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
hf : Injective ⇑f
⊢ (comap f (map f H)).relIndex K = H.relIndex K
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)

Tactic:
rw [← comap_map_eq, ← comap_map_eq, relIndex_comap, (gc_map_comap f).l_u_l_eq_l]

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_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.Data.ZMod.Basic

Goal state before:
pp: case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
⊢ Injective cast

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff',
      Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
← map_swap_divisorsAntidiagonal,

Goal state after:
n : ℕ
⊢ image Prod.snd (map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal) = n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
⊢ ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Tactic:
rcases n with - | n
  · simp
  · rcases n with - | n
    · simp at h
    · rw [or_iff_not_imp_right]
      intro ne_n
      have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
      symm
      rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]
      exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k

Tactic:
rintro ⟨j, hjk, rfl⟩

Goal state after:
case mpr
p : ℕ
pp : Prime p
k j : ℕ
hjk : j < k
⊢ (∃ k_1 ≤ k, p ^ j = p ^ k_1) ∧ p ^ j < p ^ k
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i

Tactic:
← map_swap_divisorsAntidiagonal,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (k + m).choose k ≤ (k + m + 1 - k) ^ k

Tactic:
rw [Nat.add_comm k m, Nat.add_right_comm, Nat.add_sub_cancel]

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1) ^ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case fst
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).1 = p.1

Tactic:
simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]

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

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

Tactic:
ofDigits_eq_foldr,

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

Goal state before:
pp: case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ ofDigits p (head✝ :: tail✝) ≤ ofDigits q (head✝ :: tail✝)

Tactic:
simp only [ofDigits, cast_id, add_le_add_iff_left]

Goal state after:
case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ p * ofDigits p tail✝ ≤ q * ofDigits q tail✝
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n i b : ℕ
⊢ ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)

Tactic:
List.getD_eq_getElem?_getD

Goal state after:
n i b : ℕ
⊢ ((b + 2).digits n)[i]?.getD 0 = n / (b + 2) ^ i % (b + 2)
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn₀

Goal state after:
case inl
p : ℕ
⊢ padicValNat p 0 = 0 ↔ p = 1 ∨ 0 = 0 ∨ ¬p ∣ 0

case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
refine ⟨fun L hL ↦ ?_, fun _ _ ↦ by rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]⟩

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ b.digitsAppend l (ofDigits b L) = L
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Tactic:
by
  unfold FiniteMultiplicity
  congr! 3
  simp only [dvd_neg]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1

Tactic:
isPeriodicPt_mul_iff_pow_eq_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ x ^ n = 1