mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Cycle

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

Tactic:
next,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ (y :: l).nextOr x ((y :: l).get ⟨0, ⋯⟩) = y
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
⊢ some ((x :: y :: tail).prev a ha) = (x :: y :: tail)[idxOf a (x :: y :: tail) - 1]?

Tactic:
have ih := (y :: tail).prev_eq_getElem?_idxOf_pred_of_ne_head (a := a)
    grind [prev]

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i✝ : ℕ
h₁✝ : i✝ < (pmap l.next l ⋯).length
h₂✝ : i✝ < (l.rotate 1).length
⊢ (pmap l.next l ⋯)[i✝] = (l.rotate 1)[i✝]

Tactic:
rw [getElem_pmap, getElem_rotate, next_getElem _ h]

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

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

Tactic:
by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  have lpos : 0 < l.length := k.zero_le.trans_lt hk
  have key : l.length - 1 - k < l.length := by lia
  rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]
  simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]
  rw [← getElem_pmap l.reverse.prev fun _ h => h]
  · simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
    rw [getElem_eq_getElem_reverse]
    · simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]
  · simpa

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
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
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 _ _)

Goal state after:
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
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
⊢ a :: l₁ ~ b :: l₂
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = ↑(g * 1) • x

Tactic:
mul_one

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = ↑g • x
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

Tactic:
contrapose!
    rintro hn
    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
    exact ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤ * 1

Tactic:
mul_one

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊤ = H.relIndex ⊤
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index * 1 ∣ H.index

Tactic:
mul_one

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index
Module: Mathlib.GroupTheory.Index

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

Tactic:
rw [← inf_relIndex_right] at hH hK ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0
Module: Mathlib.GroupTheory.Index

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

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H

Tactic:
· simp [index_eq_one.mp hH]

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH✝ : H.index ∣ 2
hH : H.index = 2
⊢ ∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
hf : Injective f
this : Finite (G ⧸ H)
⊢ False

Tactic:
have hcard := Nat.card_le_card_of_injective f hf

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
hf : Injective f
this : Finite (G ⧸ H)
hcard : Nat.card ↑(Set.Icc 0 H.index) ≤ Nat.card (G ⧸ H)
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

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

Tactic:
· rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = a % ↑(n✝ + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors

Tactic:
insert_self_properDivisors h

Goal state after:
n : ℕ
h : n ≠ 0
⊢ n.divisors = n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors

Tactic:
mem_filter,

Goal state after:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ n.divisors ∧ k ∣ m ↔ k ∈ m.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ m * 1 < n

Tactic:
mul_one

Goal state after:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ m < n
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]

Goal state after:
n : ℕ
⊢ image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
obtain h | h := hx.lt_or_gt

Goal state after:
case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)

Tactic:
←
    add_eq_zero_iff_eq_neg,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * 1
⊢ 2 * a.val = n✝ + 1

Tactic:
mul_one

Goal state after:
case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = n✝ + 1
⊢ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h.inr.inr
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * (n + 1).centralBinom

Tactic:
calc
    4 ^ (n + 1)
    _ = 4 * 4 ^ n := by rw [pow_succ']
    _ < 4 * (n * centralBinom n) := by gcongr; exact IH n n.lt_succ_self (Nat.le_of_lt_succ hn)
    _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
    _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ n) ^ (↑n)⁻¹.val = a

Tactic:
pow_right_comm,

Goal state after:
α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ (↑n)⁻¹.val) ^ n = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k n y : ℕ
| m * y + k = n

Tactic:
rw [add_comm, eq_comm]

Goal state after:
m k n y : ℕ
| n = k + m * y
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ ofDigits b L ≠ 0

Tactic:
contrapose w₂

Goal state after:
case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ (d :: L).getLast ⋯ = 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
by_cases hf : FiniteMultiplicity a b
  · simp [hf.emultiplicity_eq_multiplicity]
  · simp [hf, emultiplicity_eq_top.2]

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:
simp only [Nat.toDigitsCore, List.length]

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
⊢ (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
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:
simp only [Nat.toDigitsCore, List.length]

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

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ n.factorization p = padicValNat p n

Tactic:
simpa [factorization] using absurd pp

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

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

Tactic:
rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits]

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
refine ⟨fun hdn ↦ ?_, fun ⟨c, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n

case refine_2
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : d ∣ n
c : ℕ
h : n = d * c
⊢ d.factorization ≤ n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ x * 1 = 1 ↔ x = 1

Tactic:
mul_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ x = 1 ↔ x = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ (x ^ n) ^ orderOf x = 1

Tactic:
pow_right_comm,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ (x ^ orderOf x) ^ n = 1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization = f

Tactic:
by
  rw [Finsupp.prod, factorization_prod (pow_ne_zero _ <| hf · · |>.ne_zero),
    sum_congr rfl (hf · · |>.factorization_pow)]
  exact sum_single f

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
x✝ : ℕ
hp : x✝ ∈ f.support
⊢ x✝ ^ f x✝ ≠ 0

Tactic:
exact pow_ne_zero _ (prime_of_mem_primeFactors <| support_mono hf hp).ne_zero

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ List.fixedLengthDigits hb l
⊢ L.sum = (b.digits (ofDigits b L)).sum

Tactic:
rw [sum_digits_ofDigits_eq_sum hb ((List.mem_fixedLengthDigits_iff hb).mp hL)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ x ^ p = 1 ∧ ¬x * 1 = 1 ↔ x ^ p = 1 ∧ x ≠ 1

Tactic:
mul_one

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ x ^ p = 1 ∧ ¬x = 1 ↔ x ^ p = 1 ∧ x ≠ 1
Module: Mathlib.Data.Nat.Choose.Factorization

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

Tactic:
hi₁

Goal state after:
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
⊢ i < log p n + 1 → k % p ^ i + (n - k) % p ^ i < p ^ i
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (⇑n !.factorization - ⇑(k ! * (n - k)!).factorization) p = 0

Tactic:
Pi.sub_apply,

Goal state after:
case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ n !.factorization p - (k ! * (n - k)!).factorization p = 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support

Tactic:
Finsupp.mem_support_iff,

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ ¬(n.choose k).factorization p ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
by
  rcases em' p.Prime with (pp | pp)
  · simp [pp, hab]
  rcases eq_or_ne b 0 with (rfl | hb0)
  · simp
  rcases eq_or_ne a 0 with (rfl | ha0)
  · cases hb0 (zero_dvd_iff.1 hab)
  have ha := (Nat.div_pos (ordProj_le p ha0) (ordProj_pos a p)).ne'
  have hb := (Nat.div_pos (ordProj_le p hb0) (ordProj_pos b p)).ne'
  rw [← factorization_le_iff_dvd ha hb, factorization_ordCompl a p, factorization_ordCompl b p]
  intro q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp
  simp_rw [erase_ne hqp]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab q

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

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b * 1

Tactic:
mul_one

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
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 ^ n = a ^ n * 1

Tactic:
mul_one

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 ^ n
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 + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n +
      ↑p * x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)

Tactic:
by
  rw [h.add_pow_prime_pow_eq' hp, mul_assoc _ x, mul_assoc, mul_sum _ _ (_ * _)]
  congr! 3 with k hk
  obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
  rw [← mul_pow_sub_one (by lia), ← mul_pow_sub_one (n := p ^ n - k) (by lia)]
  rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ x ^ a * (x ^ b)⁻¹ = 1 ↔ x ^ a = x ^ b

Tactic:
mul_inv_eq_one

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ x ^ a = x ^ b ↔ x ^ a = x ^ b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (n + 1)! + ↑(n + 1)

Tactic:
simp only [hp, emultiplicity_factorial_mul_succ, ih, factorial_succ, emultiplicity_mul,
      cast_add, cast_one, ← add_assoc]

Goal state after:
case succ
p : ℕ
hp : Prime p
n : ℕ
ih : emultiplicity p (p * n)! = emultiplicity p n ! + ↑n
⊢ emultiplicity p n ! + ↑n + emultiplicity p (n + 1) + 1 = emultiplicity p (n + 1) + emultiplicity p n ! + ↑n + 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n = -1

Tactic:
by
  rw [eq_neg_iff_add_eq_zero]
  nth_rw 2 [← one_pow (p ^ n)]
  rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x

Tactic:
rw [← divOf_add_modOf x g, h, add_zero]

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < degree 0
⊢ P 0

Tactic:
rw [degree_zero] at h

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p : R[X]
h0 : 0 < p.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
h : 0 < ⊥
⊢ P 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (p + q)

Tactic:
rw [eq_C_of_natDegree_eq_zero hq, add_comm]

Goal state after:
case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
p q : R[X]
hp : M p
hq : q.natDegree = 0
⊢ M (C (q.coeff 0) + p)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1) * 1) = eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1)) = eval₂ C (X ^ p) (derivative f) * (↑p * X ^ (p - 1))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
have := Nontrivial.of_polynomial_ne hpq
    exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ f.coeff (n * 1) = f.coeff n

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ f.coeff n = f.coeff n
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝

Tactic:
simp_rw [coeff_add, coeff_contract hp, coeff_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * (C a - C b) = 1

Tactic:
← C_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * C (a - b) = 1
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * 1 * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

Tactic:
mul_one

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i

Tactic:
set V := fun i => U ∪ ⋂₀ σ i with hV

Goal state after:
case mp
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) * 1 = C ↑m * (X + C c) ^ (m - 1)

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ C ↑m * (X + C c) ^ (m - 1) = C ↑m * (X + C c) ^ (m - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) * 1 = C 2 * (X + C c)

Tactic:
mul_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) = C 2 * (X + C c)
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, f i ⊓ 𝓟 (s i) = ⊥) → pi f ⊓ 𝓟 (univ.pi s) = ⊥

Tactic:
simp only [inf_principal_eq_bot]

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ (∃ i, (s i)ᶜ ∈ f i) → (univ.pi s)ᶜ ∈ pi f