mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ ↑⟨(fun x ↦ x ^ N) (s' i), ⋯⟩ • x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
change s' i ^ N • x ∈ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
i : ι
hi : i ∈ ↑ι'
⊢ s' i ^ N • x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg]

Goal state after:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a - n * b ≡ c [ZMOD n] ↔ a ≡ c [ZMOD n]

Tactic:
by
  rw [← add_modulus_mul_modEq_iff, sub_add_cancel]

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

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

Tactic:
zero_mul

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 0 = 0
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
a1 : a ≠ 1
b1 : b ≠ 1
⊢ ¬Prime (a * b)

Tactic:
simp [prime_mul_iff, *]

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
h : comap f I ≤ J
⊢ Injective ⇑(quotientMap I f H)

Tactic:
refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_

Goal state after:
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
h : comap f I ≤ J
a : R ⧸ J
ha : (quotientMap I f H) a = 0
⊢ a = 0
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → l.length = n) → (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
sum_map : (map length L).sum = n * L.length
length_l : l.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
simp [sum_map, length_l, Nat.add_comm, mul_succ]

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

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

Tactic:
apply Nat.dvd_antisymm

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

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
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))

Tactic:
intro a'

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' : α
⊢ ∀ (b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a' l)) ~
      map (cons b ∘ cons c) (permutations'Aux a' l) ++
        map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a' l))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l.prev (l.next l[n] hx) ⋯ = l[n]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.next (l.prev x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l.next (l.prev l[n] hx) ⋯ = l[n]
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L

Tactic:
rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
      have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
      have ha : a ∈ b :: l₂ :=
        mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂
          (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
      have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
      have hl : prod l₁ = prod ((b :: l₂).erase a) :=
        (mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by
          rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
      exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm

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

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False

Tactic:
zero_mul

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case mk.mk
G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x✝¹ : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ∃ g, g • Quot.mk (⇑(leftRel H)) x = Quot.mk (⇑(leftRel H)) y

Tactic:
refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩

Goal state after:
case mk.mk
G✝ : Type u
X : Type v
inst✝² : Group G✝
inst✝¹ : MulAction G✝ X
x✝¹ : X
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ((fun x_1 ↦ (y * x⁻¹) • x_1) x)⁻¹ * y ∈ H
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'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ (comap f J).relIndex (comap f K) ≠ 0

Tactic:
rw [relIndex_comap]
  exact fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Tactic:
← range_subtype L,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L.subtype.range).relIndex (K ⊓ L.subtype.range) ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ↑(a % ↑b) = ↑a

Tactic:
ZMod.intCast_eq_intCast_iff

Goal state after:
a : ℤ
b : ℕ
⊢ a % ↑b ≡ a [ZMOD ↑b]
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (x • y) • z = x • y • z

Tactic:
by rw [Algebra.smul_def, mul_smul]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ n / b < n / a

Tactic:
Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
a b : ℕ
hab : a < b
ha : a * (n / a) = n
hb : b * (n / b) = n
⊢ a < b
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
exact mul_ne_zero_iff.mp (hp₁.symm ▸ hp₂)

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
· rw [hx, neg_one_geom_sum]
    simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rintro ⟨x, y⟩

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

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

Tactic:
rintro ⟨x, y⟩

Goal state after:
case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
x : ZMod 1
y : ZMod 0
⊢ to_fun (inv_fun (x, y)) = (x, y)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 * (b - 1) ≤ a * b

Tactic:
zero_mul

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ n.centralBinom ≤ 4 ^ n

Tactic:
grw [show 4 = 2 ^ 2 by rfl, ← pow_mul, centralBinom_eq_two_mul_choose, choose_le_two_pow]

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (n + a.val - b.val) % n = a.val - b.val

Tactic:
Nat.add_sub_assoc h,

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (n + (a.val - b.val)) % n = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

pp: case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
· cases w

Goal state after:
case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: p n : ℕ
⊢ (p.digits n).sum ≤ n

Tactic:
by
  induction n with
  | zero => exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  | succ n =>
    induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ emultiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
by
  rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b

Tactic:
by
  induction l <;> simp [Nat.ofDigits]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < emultiplicity a b
⊢ n < multiplicity a b

Tactic:
by
  rw [emultiplicity_eq_multiplicity hfin] at h
  assumption_mod_cast

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ¬FiniteMultiplicity a b

Tactic:
simp [FiniteMultiplicity]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
by
  conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
  rw [coe_ofDigits]
  apply ofDigits_zmodeq' _ _ _ h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
rw [IsPeriodicPt, IsFixedPt, mul_left_iterate_apply_one]

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

Goal state before:
pp: n e : ℕ
⊢ 0 < e → n < 10 ^ e → n.repr.length ≤ e

Tactic:
by
  simpa [Nat.repr] using toDigits_length _ _ _

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
· rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ x ^ a = x ^ (a + c)

Tactic:
obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h

Goal state after:
case inl
G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + n * c [MOD n]
hle : a ≤ a + n * c
⊢ x ^ a = x ^ (a + n * c)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ x ^ (b + c) = x ^ b

Tactic:
obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + n * c ≡ b [MOD n]
hle : b ≤ b + n * c
⊢ x ^ (b + n * c) = x ^ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
rw [h0, coprime_zero_right] at h

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (p : ℕ), b.factorization p ≤ a.factorization p
⊢ b ≤ a

Tactic:
← Finsupp.le_def,

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b.factorization ≤ a.factorization
⊢ b ≤ a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

pp: case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
· simp [zero_dvd_iff.mp h]

Goal state after:
case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * ∑ i ∈ Ioo 0 (p ^ n), x * y * (x ^ (i - 1) * y ^ (p ^ n - i - 1) * ↑((p ^ n).choose i / p))

Tactic:
congr! 3 with k hk

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
⊢ x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p))
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:
Set.mem_toFinset,

Goal state after:
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✝)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Ring G
inst✝¹ : LinearOrder G
inst✝ : IsStrictOrderedRing G
a : G
ha₀ : a ≤ 0
ha : IsOfFinOrder a
⊢ ¬a = 1

Tactic:
by
    rintro rfl; exact one_pos.not_ge ha₀

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ p.divX.degree < p.degree

Tactic:
have := Nontrivial.of_polynomial_ne hp0
  calc
    degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
      if h : degree p ≤ 0 then by
        have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
      else by
        have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
    _ = degree p := congr_arg _ (divX_mul_X_add _)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ 0 * ↑n = 0

Tactic:
zero_mul

Goal state after:
case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M (0 * X)

Tactic:
zero_mul

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : ¬p.coeff 0 = 0
hpX0 : p.divX = 0
⊢ M 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ 0 = 0 * p

Tactic:
zero_mul

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (0 * if n = 0 - 1 then 1 else 0) = 0

Tactic:
zero_mul

Goal state after:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p %ₘ 0 = p

Tactic:
have := monic_zero_iff_subsingleton.mp h

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p %ₘ 0 = p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic 0
⊢ p /ₘ 0 = 0

Tactic:
have := monic_zero_iff_subsingleton.mp h

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
this✝ : DecidableEq R := Classical.decEq R
h : Monic 0
this : Subsingleton R
⊢ p /ₘ 0 = 0