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

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩

Goal state after:
case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (p * (q * q'))) v = ((aeval f) (q' * (p * q))) v

Tactic:
by rw [← mul_assoc, mul_comm]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ n ∣ a ↔ n ∣ b

Tactic:
by
  simp only [← modEq_zero_iff_dvd]
  exact ⟨fun ha ↦ h.symm.trans ha, h.trans⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0

Tactic:
rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]

Goal state after:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

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

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
· intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotQuotMk I J) = I ⊔ J

Tactic:
RingHom.ker_eq_comap_bot,

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ comap (quotQuotMk I J) ⊥ = I ⊔ J
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a = b

Tactic:
rw [← sub_eq_zero]

Goal state after:
M : Type u_1
G : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup G
inst✝ : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a - b = 0
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty (Unique (orbitRel.Quotient G α))

Tactic:
by
  rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
  exact fun _ ↦ (nonempty_quotient_iff _).mpr inferInstance

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂

Tactic:
rw [eq_of_heq hxy]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
· obtain ⟨x, hx1, hx2⟩ := L_ih hd
        exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c

Tactic:
Cycle.chain_coe_cons,

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : IsChain r (a :: (l ++ [a]))
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
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:
by rwa [primeFactorsList] at h

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

Goal state after:
case inl.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

Tactic:
rw [← inv_mem_iff (x := a), ← ha, inv_mul_cancel]
    exact one_mem _

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = Nat.card G

Tactic:
← index_bot

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = ⊥.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ ↑a.cast = a

pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a

Tactic:
· simp [ZMod.cast, ZMod]

Goal state after:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑a.cast = a
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H

Tactic:
convert! he

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ ↑(n₂ - n₁) = ↑n₂ + -↑n₁
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
this : ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G✝ : Type u_1
G' : Type u_2
inst✝² : Group G✝
inst✝¹ : Group G'
H✝ K L : Subgroup G✝
f : G✝ →* G'
G : Type u_3
inst✝ : AddGroup G
H : AddSubgroup G
h : H.FiniteIndex
⊢ H.normalCore.FiniteIndex

Tactic:
by
  rw [← AddSubgroup.finiteIndex_toSubgroup_iff] at h ⊢
  exact H.toSubgroup.finiteIndex_normalCore

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

Goal state before:
pp: case mpr
p n : ℕ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = z.val + p * k) → ↑n = z

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℕ
⊢ ↑(z.val + p * k) = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z

Tactic:
rintro ⟨k, rfl⟩

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑z.val + ↑p * k) = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑z.val + ↑p * ↑k = z

Tactic:
natCast_val,

Goal state after:
case mpr
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ z.cast + ↑p * ↑k = z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝ : ℤ
⊢ x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ ↑n ∣ x✝

Tactic:
AddMonoidHom.mem_ker,

Goal state after:
n : ℕ
x✝ : ℤ
⊢ (Int.castAddHom (ZMod n)) x✝ = 0 ↔ ↑n ∣ x✝
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a * b).val = a.val * b.val

Tactic:
apply Int.natAbs_mul

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).divisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
ext a
  rw [mem_divisors_prime_pow pp]
  simp [eq_comm]

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

Goal state before:
pp: case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n

Tactic:
· exact (Nat.choose_lt_two_pow _ _ hn).le

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

Goal state before:
pp: case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
rw [digits_getLast n (le_add_left 2 b)]

Goal state after:
case neg
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 2).digits (n / (b + 2))).getLast ?neg.q✝ ≠ 0

case neg.q
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ (b + 2).digits (n / (b + 2)) ≠ []
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < n + 1

pp: case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))

Tactic:
· apply Nat.div_lt_self <;> lia

Goal state after:
case ind.succ.tail.a
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))
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 ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
rw [← ofDigits_one <| digits p.succ n.succ]

Goal state after:
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
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | _

Goal state after:
case neg.zero
b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits 0).head! = 0 % b

case neg.succ
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n✝ : ℕ
⊢ (b.digits (n✝ + 1)).head! = (n✝ + 1) % b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
| succ f ih =>

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
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
| succ f ih =>

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

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore (f + 1) n []).length ≤ e

Tactic:
| succ f ih =>

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
rw [ha] at h; exact h 1

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b

Tactic:
simp [fixedLengthDigits]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ ∈ fixedLengthDigits hb 0 ↔ a✝ ∈ {[]}

Tactic:
simp [fixedLengthDigits]

Goal state after:
b : ℕ
hb : 1 < b
a✝ : List ℕ
⊢ a✝ = [] → ∀ x ∈ a✝, x < b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

pp: case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
· simp [pp, hab]

Goal state after:
case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]

Tactic:
this (le_of_not_ge hmn)

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]

Tactic:
this (le_of_not_ge hmn)

Goal state after:
case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]

Tactic:
this (le_of_not_ge hmn)

Goal state after:
case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}

Tactic:
simp only [Finset.mem_filter, mem_Ico, and_congr_left_iff, and_congr_right_iff]

Goal state after:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x✝ : G
inst✝ : DecidableEq G
this : Fintype ↥(zpowers x✝) := (zpowers x✝).instFintypeSubtypeMemOfDecidablePred
x : G
⊢ x ∈ Finset.image (fun i ↦ x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ (↑(zpowers x✝)).toFinset

Tactic:
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ C (p.coeff 0) ≠ 0

Tactic:
rwa [← eq_C_of_degree_le_zero h]

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

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)

Tactic:
by
  set g := gcd m n
  let m' := m / gcd m n
  let n' := n / gcd m n
  have coprime : m'.Coprime n' := by
    rcases hmn with hm | hn
    · exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)
    · exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)
  have pow_eq : a ^ m' = b ^ n' := by
    conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
    conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
    rw [pow_mul, pow_mul] at h
    have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
    exact Nat.pow_left_injective this h
  exact exists_eq_pow_of_exponent_coprime_of_pow_eq_pow coprime pow_eq

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

Goal state before:
pp: case pos.inl
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
nontriviality R

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
nontriviality R

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
nontriviality R

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree + (p /ₘ q).degree = p.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑t.card + 1 ≤ (X - C x).degree + (p /ₘ (X - C x)).degree

Tactic:
degree_X_sub_C,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ↑t.card + 1 ≤ 1 + (p /ₘ (X - C x)).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ q.degree + (p /ₘ q).degree

Tactic:
degree_eq_natDegree hq.ne_zero,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ ↑q.natDegree ≤ ↑q.natDegree + (p /ₘ q).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ q.degree + (p /ₘ q).degree

Tactic:
degree_eq_natDegree hq.ne_zero,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ ↑q.natDegree + (p /ₘ q).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < q.degree + (p /ₘ q).degree

Tactic:
degree_eq_natDegree hq.ne_zero,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < ↑q.natDegree + (p /ₘ q).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
nontriviality R

Goal state after:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
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
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
nontriviality R

Goal state after:
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
⊢ f /ₘ g = q ∧ f %ₘ g = r
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ Transcendental R x ↔ ∀ (p : R[X]), (aeval x) p = 0 → p = 0

Tactic:
by
  rw [Transcendental, IsAlgebraic, not_exists]
  congr! 1; tauto

Goal state after: