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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ Function.RightInverse (fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) fun p ↦ ⟨(↑p).eraseLead, ⋯⟩

Tactic:
by
    rintro ⟨p, hp⟩
    ext1
    simp only
    rw [eraseLead_add_of_degree_lt_left]
    · simp
    · simp [mem_degreeLT.1 hp]

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

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
⊢ ∃ n, (f * g).coeff n ∉ P

Tactic:
let m := Nat.find hf

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
⊢ ∃ n, (f * g).coeff n ∉ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∃ n, (f * g).coeff n ∉ P

Tactic:
refine ⟨m + n, ?_⟩

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ (f * g).coeff (m + n) ∉ P
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
by
  refine .trans ‹_› ⟨{Polynomial.X}, ?_⟩
  rw [Finset.coe_singleton]
  exact Polynomial.adjoin_X

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M

Tactic:
refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ p.support
this : C (coeff m p) ∈ I
⊢ C (coeff m p) * (monomial m) 1 ∈ I

Tactic:
by exact I.mul_mem_right (monomial m 1) this

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

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
x✝ : R ⧸ ker f
x : R
⊢ (⇑(Ideal.Quotient.mk (ker f)) ∘ g) (f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x)) =
    Quot.mk (⇑(Submodule.quotientRel (ker f))) x

Tactic:
apply kerLift_injective

Goal state after:
case mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
x✝ : R ⧸ ker f
x : R
⊢ f.kerLift ((⇑(Ideal.Quotient.mk (ker f)) ∘ g) (f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x))) =
    f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x)
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 2 * x = 0

Tactic:
two_eq_zero,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 0 * x = 0
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)

Tactic:
induction ts with

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd

Tactic:
induction ts with

Goal state after:
case cons
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) ts.permutations' = (map f ts).permutations'

Tactic:
induction ts with

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r

Tactic:
exact (Nat.lt_div_mul_add hr).le

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

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

Tactic:
· apply Coprime.dvd_of_dvd_mul_right (coprime_div_gcd_div_gcd h)
    apply Nat.dvd_of_mul_dvd_mul_right h
    rw [Nat.div_mul_cancel (gcd_dvd_left _ _), mul_assoc, Nat.div_mul_cancel (gcd_dvd_right _ _),
      mul_comm]
    apply IsPeriodicPt.minimalPeriod_dvd
    rw [IsPeriodicPt, IsFixedPt, iterate_mul]
    exact isPeriodicPt_minimalPeriod _ _

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 : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b : A
hb : b ∈ adjoin R s
⊢ p ⟨b, hb⟩

Tactic:
induction hb using adjoin_induction with
    | mem _ h => exact mem _ h
    | algebraMap _ => exact algebraMap _
    | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂
    | star _ _ h => exact star _ h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
⊢ ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'

Tactic:
intro xs'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
⊢ (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

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

Tactic:
· exact (isPeriodicPt_minimalPeriod _ _).mul_const _

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.length + 1 = (s.insertIdx (k + 1) x).length

Tactic:
length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ s.length + 1 = s.length + 1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ (permutations'Aux x ys).Nodup

Tactic:
rw [nodup_permutations'Aux_iff, hy.mem_iff]

Goal state after:
case cons.left
α : 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
ys : List α
hy : ys ~ l
⊢ ¬x ∈ l
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : 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.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (Disjoint on permutations'Aux x) as bs

Tactic:
Function.onFun,

Goal state after:
case cons.right
α : 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.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (permutations'Aux x as).Disjoint (permutations'Aux x bs)
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 β
x : orbitRel.Quotient G α
⊢ ∀ (x_1 y : ↑x.orbit), ∃ g, g • x_1 = y

Tactic:
by
    induction x using Quotient.inductionOn'
    rintro ⟨y, yh⟩ ⟨z, zh⟩
    rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh
    rcases yh with ⟨g, rfl⟩
    rcases zh with ⟨h, rfl⟩
    refine ⟨h * g⁻¹, ?_⟩
    ext
    simp [mul_smul]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯

Tactic:
by
  ext x; simp [stabilizerEquivStabilizer]

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

Goal state before:
pp: α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l

Tactic:
rw [lists, Quotient.liftOn'_mk'']

Goal state after:
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑l.cyclicPermutations ↔ ↑l✝ = Quotient.mk'' l
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Cycle α
a b : List α
hab : (IsRotated.setoid α) a b
⊢ (match a with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
by
      rcases a with - | ⟨a, l⟩ <;> rcases b with - | ⟨b, m⟩
      · rfl
      · have := isRotated_nil_iff'.1 hab
        contradiction
      · have := isRotated_nil_iff.1 hab
        contradiction
      · dsimp only
        obtain ⟨n, hn⟩ := hab
        induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

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
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ Quotient.mk'' ↑x = ω

Tactic:
@Quotient.mk''_eq_mk

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x✝ : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ ⟦↑x⟧ = ω
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : Quotient.mk'' ↑a = Quotient.mk'' ↑b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
@Quotient.mk''_eq_mk

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
by
  simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
exact relIndex_mul_index fun x hx => hHK hx

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
this : NeZero n
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
apply ZMod.castHom_injective

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
⊢ ∃ n, 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Tactic:
rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩
  refine ⟨n, hlt, hle, ?_⟩
  simpa [pow_mem ha, mem_subgroupOf] using he

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [le_add_iff_nonneg_left]

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0

Tactic:
by
  obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
  exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.snd z.divisorsAntidiag = z.divisors

Tactic:
ext
  simp [Eq.comm, mul_comm, dvd_def]

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

Goal state before:
pp: b n : ℕ
⊢ ofDigits b [n] = n

Tactic:
by simp [ofDigits]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = ↑h + ofDigits 1 L

Tactic:
by simp [ofDigits]

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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Tactic:
induction l1 with

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

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1

Tactic:
intro n c tl

Goal state after:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
intro n c tl

Goal state after:
case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ¬a ∣ c

Tactic:
rintro ⟨k, hk⟩

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head?.getD default = n.succ / (b + 2) ^ default % (b + 2)

Tactic:
← List.head!_eq_head?_getD,

Goal state after:
case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ ((b + 2).digits n.succ).head! = n.succ / (b + 2) ^ default % (b + 2)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0

Tactic:
by
  rwa [orderOf, minimalPeriod, dif_neg]

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) = (l + 1) * b ^ l * (b * (b - 1) / 2)

Tactic:
show b ^ l = b * b ^ (l - 1) by rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'

Goal state after:
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, a.factorization p < b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
have h0 : 2 ≤ p := hp.two_le
  have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
  have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
  have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
  have h4 m (hm : m ∈ Ico (p * n + 1) (p * (n + 1))) : m.factorization p = 0 := by
    apply factorization_eq_zero_of_not_dvd
    exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right
  rw [← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), ← sum_Ico_consecutive _ h1 h3, add_assoc, sum_Ico_succ_top h2,
    ← prod_Ico_id_eq_factorial, factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left), factorization_mul (ne_zero_of_lt h0) (zero_ne_add_one n).symm,
    coe_add, Pi.add_apply, hp.factorization_self, sum_congr rfl h4, sum_const_zero, zero_add,
    add_comm 1]

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
hx : IsOfFinOrder x
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x
⊢ orderOf (x * y) = orderOf x

Tactic:
by
  simpa [h.eq] using
    orderOf_mul_eq_right_of_forall_prime_mul_dvd (x := y) (y := x) h.symm hx hdvd

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (m + (n - m)) = a ^ m * 1

Tactic:
add_tsub_cancel_of_le hmn.le,

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ n = a ^ m * 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
n : ℕ
hn : n ≠ 0
⊢ ∃ x x_1, ∃ (_ : Prime x) (_ : x ^ x_1 ∣ 0), ¬x ^ x_1 ∣ n

Tactic:
exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_ge⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (↑n.divisors).PairwiseDisjoint fun m ↦ {x | orderOf x = m}

Tactic:
simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]

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

Goal state before:
pp: case hfg
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∀ x ∈ n.factorization.support, (fun x1 x2 ↦ x1 ^ x2) x (n.factorization x) = x ^ padicValNat x n

Tactic:
intro p hp
    simp [factorization_def n (prime_of_mem_primeFactors hp)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
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
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
by
    have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
    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:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
hm0 : ¬m = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
· use 0
      simp_all

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p * C q.leadingCoeff

Tactic:
by
  obtain ⟨r, rfl⟩ := hdvd
  obtain rfl | hr := eq_or_ne r 0
  · simp
  have : r.natDegree = 0 := by simpa [hp.natDegree_mul' hr] using hdeg
  rw [eq_C_of_natDegree_eq_zero this]
  simp [leadingCoeff_monic_mul hp]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : (X - C c) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p.comp (C a * X + C b)
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p

Tactic:
dvd_comp_C_mul_X_add_C_iff,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
h : ((X - C c) ^ rootMultiplicity c (p.comp (C a * X + C b))).comp (C ⅟a * (X - C b)) ∣ p
⊢ (X - C (a * c + b)) ^ rootMultiplicity c (p.comp (C a * X + C b)) ∣ p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
simp_rw [mem_image, mem_antidiagonal]

Goal state after:
case hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n * p → (¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree

Tactic:
simp [h₁]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∀ (n : ℕ), C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
all_goals intro n; rw [zero_mul, C_0, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
by
          rw [Nat.succ_add_eq_add_succ]

Goal state after: