mathlib-initiative/mathlib-tactics huggingface dataset:
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 + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
      try assumption

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

Tactic:
by_cases hf : f = 0
  · rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
  apply le_antisymm
  · refine tsub_le_iff_right.mp ?_
    apply le_natDegree_of_ne_zero
    rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
    exact trailingCoeff_nonzero_iff_nonzero.mpr hf
  · rw [← le_tsub_iff_left f.reverse_natDegree_le]
    apply natTrailingDegree_le_of_ne_zero
    have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
    rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

Tactic:
simp only [← coeff_one_reverse]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

case neg
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
⊢ q - r = 0

Tactic:
← hp.mul_right_eq_zero_iff,

Goal state after:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : p * q = p * r
⊢ p * (q - r) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
h✝ : CharP R p
h : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
n : ℕ
⊢ C ↑n = 0 ↔ p ∣ n

Tactic:
← C_0,

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
p : ℕ
h✝ : CharP R p
h : ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
n : ℕ
⊢ C ↑n = C 0 ↔ p ∣ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ≠ 0

Tactic:
ne_eq

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ ¬x = 0
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : ⊤.FG
hSA : ⊤.FG
⊢ ⊤.FG

Tactic:
classical
  rcases hRS with ⟨s, hs⟩
  rcases hSA with ⟨t, ht⟩
  exact ⟨s.image (algebraMap S A) ∪ t, by
    rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
    ⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(if p.coeff n = 0 then 0 else ⟨p.coeff n, ⋯⟩) = p.coeff n

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
⊢ ↑(p.restriction.coeff i) = 0

Tactic:
H,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
H : p.restriction.coeff i = 0
⊢ ↑0 = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
⊢ ↑(p.restriction.coeff p.natDegree) = 1

Tactic:
H,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
H : p.restriction.coeff p.natDegree = 1
⊢ ↑1 = 1
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:
by
  rw [leadingCoeff, Submodule.mem_iSup_of_directed]
  · simp only [mem_leadingCoeffNth]
    constructor
    · rintro ⟨i, p, hpI, _, rfl⟩
      exact ⟨p, hpI, rfl⟩
    rintro ⟨p, hpI, rfl⟩
    exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩
  intro i j
  exact
    ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
      I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) m

Tactic:
have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : SetLike S R
hSR : NonUnitalSubsemiringClass S R
s : S
this : SMulMemClass S ℕ R
⊢ (unitization s).range = subalgebraOfSubsemiring (Subsemiring.closure ↑s)

Tactic:
rw [unitization, NonUnitalSubalgebra.unitization_range (hSRA := this), Algebra.adjoin_nat]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
⊢ Function.Injective fun x ↦ x ^ 2

Tactic:
intro x y h
  rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

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

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

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

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

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Tactic:
· by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

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

Goal state before:
pp: case succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Tactic:
refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h

Goal state after:
case succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'

case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
⊢ (if x = y then z else (z :: zs).nextOr x d) ∈ xs'

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, gp✝⟩ • b✝ ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)

Goal state after:
case refine_2.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ?refine_2.refine_1⟩ ∈ H.subgroupOf K
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.prev x ⋯

Tactic:
← next_reverse_eq_prev _ (h.nodup_iff.mp hn)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l'.reverse.next x ⋯
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
x✝ : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer ⋯) x✝) = ↑((MulEquiv.refl ↥(stabilizer G a)) x✝)

Tactic:
simp [stabilizerEquivStabilizer_apply]

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

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]

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

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList

Tactic:
rwa [primeFactorsList] at h

Goal state after:
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 : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]

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 : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ g₁⁻¹ • x ∈ orbit (↥H) (g₂⁻¹ • x)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case h
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
a✝ : X
⊢ ⟦⋯.choose⁻¹ • x⟧ = Quotient.mk'' a✝

Tactic:
rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]

Goal state after:
case h
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
a✝ : X
⊢ ⋯.choose⁻¹ • x ∈ orbit (↥H) a✝
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rw [mul_comm]
  exact mem_primeFactorsList_mul_left hpb ha

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
simp only [index_eq_two_iff, xor_iff_or_and_not_and]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), (b * a ∈ H ∨ b ∈ H) ∧ ¬(b * a ∈ H ∧ b ∈ H)) ↔ ∃ a ∉ H, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
n0 : n ≠ 0
a : ℕ
⊢ addOrderOf ↑(a + 1) = n / n.gcd (a + 1)

Tactic:
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: case succ
n : ℕ
a b : Fin (n + 1)
⊢ ↑(if n + 1 ≤ ↑a + ↑b then ↑a + ↑b - (n + 1) else ↑a + ↑b) =
    if n + 1 ≤ ↑a + ↑b then cast a + cast b - ↑(n + 1) else cast a + cast b

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
a b : Fin (n + 1)
h : n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b - (n + 1)) = cast a + cast b - ↑(n + 1)

case neg
n : ℕ
a b : Fin (n + 1)
h : ¬n + 1 ≤ ↑a + ↑b
⊢ ↑(↑a + ↑b) = cast a + cast b
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝² : Ring R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Module (ZMod n) R
r : ZMod n
x : R
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
obtain _ | n := n

Goal state after:
case zero
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
inst✝ : Module (ZMod 0) R
r : ZMod 0
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

case succ
R✝ : Type u_1
inst✝² : Ring R✝
R : Type u_2
inst✝¹ : Ring R
x : R
n : ℕ
inst✝ : Module (ZMod (n + 1)) R
r : ZMod (n + 1)
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonalList.toFinset ↔ a.1 * a.2 = n ∧ n ≠ 0

Tactic:
toFinset_divisorsAntidiagonalList,

Goal state after:
n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonal ↔ a.1 * a.2 = n ∧ n ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ + ↑n.succ * ↑(a.val.gcdB n.succ) = ↑(↑a.val * a.val.gcdA n.succ + ↑n.succ * a.val.gcdB n.succ)

Tactic:
push_cast
        rw [natCast_zmod_val]
        rfl

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:
by
      gcongr with i hi
      rw [pow_succ, ← Nat.div_div_eq_div_mul]
      exact Nat.div_mul_le_self _ _

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

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ (if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x.cast).cast else ((RingHom.fst (ZMod m) (ZMod n)) x.cast).cast
    else ↑↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val)) =
    ↑x.val

Tactic:
if_neg hmn0,

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑↑(Nat.chineseRemainder h x.cast.1.val x.cast.2.val) = ↑x.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod n) M)

Tactic:
obtain _ | n := n

Goal state after:
case zero
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod 0) M)

case succ
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
⊢ Subsingleton (Module (ZMod (n + 1)) M)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ (l + 1) ∣ b
⊢ False

Tactic:
exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = ⊤ ↔ ¬FiniteMultiplicity a b

Tactic:
simp [emultiplicity]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ emultiplicity ↑a ↑b = emultiplicity a b

Tactic:
by
  unfold emultiplicity FiniteMultiplicity
  congr! <;> norm_cast

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

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

Tactic:
by
  induction L with
  | nil => rfl
  | cons d L ih =>
    dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.left
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ a ^ n ∣ b

pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b

Tactic:
· apply pow_dvd_of_le_emultiplicity
      simp [h]

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ¬a ^ (n + 1) ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1

Tactic:
exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩

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

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
⊢ i < b

Tactic:
obtain hi | ⟨_, rfl⟩ := hi

Goal state after:
case inl
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b

case inr
n b : ℕ
hb : 1 < b
l : ℕ
left✝ : l - (b.digits n).length ≠ 0
⊢ 0 < b
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
exact List.replicate_sublist_iff.mpr le_rfl |>.subperm

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False

pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
· have : IsUnit a := .of_mul_eq_one v hv.symm
      simpa [this] using ha.not_isUnit

Goal state after:
case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ n.factorization p

Tactic:
simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

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

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
if hb : b = 0 then simp [hb] else
  simp only [ordProj_mul p ha hb]
  rw [div_mul_div_comm (ordProj_dvd a p) (ordProj_dvd b p)]

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
⊢ n.factorization p < n

Tactic:
by_cases pp : p.Prime
  · exact (Nat.pow_lt_pow_iff_right pp.one_lt).1 <| (ordProj_le p hn).trans_lt <|
      Nat.lt_pow_self pp.one_lt
  · simpa only [factorization_eq_zero_of_not_prime n pp] using! hn.bot_lt

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
by_cases h0 : orderOf x = 0
  · rw [h0, lcm_zero_left]
    apply dvd_zero
  conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]
  exact
    (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
      (Nat.lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (Nat.dvd_lcm_left _ _), Nat.dvd_lcm_right _ _⟩)

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

Goal state before:
pp: case pos
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n

pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
· simp [n_zero]

Goal state after:
case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ 2 * p + (k % p + (n - k) % p) < 2 * p + p

Tactic:
← succ_mul,

Goal state after:
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ 2 * p + (k % p + (n - k) % p) < succ 2 * p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ orderOf (-1) = if ringChar R = 2 then 1 else 2

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1

case neg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n.centralBinom.factorization p = 0

Tactic:
refine factorization_choose_of_lt_three_mul ?_ p_le_n (p_le_n.trans ?_) big
  · lia
  · rw [two_mul, add_tsub_cancel_left]

Goal state after: