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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail✝ fun x ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x ↦ f' (g ys_hd :: x)).snd

Tactic:
ys_ih

Goal state after:
case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) ?cons.f').snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x ↦ f' (g ys_hd :: x)).snd

case cons.f'
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ List α' → β'

case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = ?cons.f' (map g a)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun y ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap,
    append_assoc, cons_append]

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!

Tactic:
intro t

Goal state after:
α : Type u_1
t : α
⊢ ∀ (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + [].length ! = (is.length + [].length)! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
intro t

Goal state after:
α : Type u_1
t : α
⊢ ∀ (ts is : List α),
    (∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem
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 x✝ : A
h : x✝ ∈ s
⊢ p ⟨x✝, ⋯⟩

Tactic:
exact mem _ h

Goal state after:
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' : α
⊢ map (fun x ↦ b' :: c :: x) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (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:
exact Perm.refl _

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

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (permutations'Aux y✝) (flatMap (permutations'Aux x✝) l✝.permutations') ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')

Tactic:
rw [flatMap_assoc, flatMap_assoc]

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x ↦ flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (fun x ↦ flatMap (permutations'Aux x✝) (permutations'Aux y✝ x)) l✝.permutations'
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 (StarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
by
  simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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

Goal state before:
pp: n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList <+ (n * k).primeFactorsList

Tactic:
by
  rcases n with - | hn
  · simp [zero_mul]
  apply sublist_of_subperm_of_pairwise _
    (primeFactorsList_sorted _).pairwise (primeFactorsList_sorted _).pairwise
  simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]
  exact (sublist_append_left _ _).subperm

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (f x) = Quotient.mk'' (f y)
⊢ Injective (Quotient.map' ⇑f ⋯)

Tactic:
refine Quotient.ind' fun x => ?_

Goal state after:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key✝ : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
key : ∀ (x y : G'), Quotient.mk'' x = Quotient.mk'' y ↔ Quotient.mk'' (f x) = Quotient.mk'' (f y)
x : G'
⊢ ∀ ⦃a₂ : G' ⧸ comap f H⦄, Quotient.map' ⇑f ⋯ (Quotient.mk'' x) = Quotient.map' ⇑f ⋯ a₂ → Quotient.mk'' x = a₂
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
refine Quotient.ind' fun x => ?_

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
x : G
⊢ ∃ a, Quotient.map' ⇑f ⋯ a = Quotient.mk'' x
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
· refine Quotient.ind' fun x => ?_
    obtain ⟨y, hy⟩ := hf x
    exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

pp: case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast

Tactic:
· exact congr_arg (Int.cast ∘ ·) ZMod.cast_id'

Goal state after:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast
Module: Mathlib.GroupTheory.Index

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

Tactic:
index_dvd_two_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), b * a ∈ H ∨ b ∈ H) ↔ ∃ a, ∀ (b : G), a * b ∈ H ∨ b ∈ H
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
⊢ n ≠ 0

Tactic:
intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0

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

Goal state before:
pp: a : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)

Tactic:
by
  cases a <;> rfl

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 : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n
⊢ a ^ n ∈ H ⊓ K

Tactic:
by
  convert! pow_mem_of_index_ne_zero_of_dvd h ⟨a, ha⟩ hn
  simp [pow_mem ha, mem_subgroupOf]

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

Goal state before:
pp: m n : ℕ
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
suffices (m % n).gcd n = m.gcd n by grind

Goal state after:
m n : ℕ
⊢ (m % n).gcd n = m.gcd n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k✝ : ℕ
k : ℕ × ℕ
⊢ k ∈ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k✝) →
    k ∈ (q ^ k✝).divisorsAntidiagonal

Tactic:
hk

Goal state after:
q : ℕ
hq : 1 < q
k✝ : ℕ
k : ℕ × ℕ
hk : k ∈ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k✝)
⊢ k ∈ (q ^ k✝).divisorsAntidiagonal
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k : ℕ
⊢ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal

Tactic:
intro k hk
  obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk
  simp [Nat.mem_divisorsAntidiagonal, ← Finset.mem_antidiagonal.mp hi, pow_add, ne_zero_of_lt hq]

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

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
by
  rcases le_or_gt k n with h | h
  · obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le h
    rw [Nat.add_comm k m, Nat.add_right_comm, Nat.add_sub_cancel]
    exact choose_add_le_add_one_pow m k
  · simp [choose_eq_zero_of_lt h]

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

Goal state before:
pp: n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ x.natAbs ≤ y.natAbs

Tactic:
sub_eq_iff_eq_add

Goal state after:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ x.natAbs ≤ y.natAbs
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
hb : 1 < b
L1 L2 : List ℕ
len : L1.length = L2.length
w1 : ∀ l ∈ L1, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b L1 = ofDigits b L2
⊢ L1 = L2

Tactic:
induction L1 generalizing L2 with
  | nil =>
    simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  | cons D L ih => ?_

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
⊢ D :: L = L2
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1

Tactic:
rw [digits_eq_cons_digits_div hb hn, List.length]

Goal state after:
case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl

Goal state after:
case inl.cons.inr
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,

Goal state after:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ ↑n ≤ emultiplicity a b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Tactic:
unfold FiniteMultiplicity

Goal state after:
α : Type u_1
inst✝ : Ring α
a b : α
⊢ (∃ n, ¬a ^ (n + 1) ∣ -b) ↔ ∃ n, ¬a ^ (n + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L.head ⋯ = d

Tactic:
by
  obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL
  rw [head_cons]

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

Goal state before:
pp: p : ℕ
hp : Prime p
q : ℕ
⊢ count q [p] = (single p 1) q

Tactic:
single_apply,

Goal state after:
p : ℕ
hp : Prime p
q : ℕ
⊢ count q [p] = if p = q then 1 else 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)

Tactic:
by simp [hs, pow_add, mul_comm, mul_left_comm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ multiplicity p a = 0

Tactic:
apply Nat.eq_zero_of_not_pos

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ ¬0 < multiplicity p a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
⊢ n.factorization p ≤ b

Tactic:
by
  if hn : n = 0 then simp [hn] else
  if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]

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

Goal state before:
pp: case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ a.factorization p ≤ b.factorization p

Tactic:
exact (factorization_le_iff_dvd ha0 hb0).2 hab p

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ emultiplicity p (n.choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}))

Tactic:
have := Nat.sub_add_cancel hkn

Goal state after:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p (n.choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}))
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
⊢ a.factorization p = (c ^ n).factorization p

Tactic:
have foo (p) (hp : p ∈ factors.support) : Prime p :=
    prime_of_mem_primeFactors (Finsupp.support_mapRange hp)

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ a.factorization p = (c ^ n).factorization p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree

Tactic:
divByMonic_eq_zero_iff hg

Goal state after:
case pos
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
divByMonic_eq_zero_iff hg

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R p) f) = p * rootMultiplicity (r ^ p) f

Tactic:
by
  rw [← pow_one p, rootMultiplicity_expand_pow]

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:
rw [Nat.succ_add_eq_add_succ]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
⊢ ∀ (t : Set α), t ∈ ⨅ i, l i ↔ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
intro t

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨅ i, l i ↔ ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
⊢ ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) =
    ∑ k ∈ range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
refine sum_congr_of_eq_on_inter (fun k hk hk' ↦ ?_) (by simp_all) (by simp)

Goal state after:
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k)) = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
l : ι → Filter α
t : Set ι
hd : t.PairwiseDisjoint l
ht : t.Finite
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s

Tactic:
have := ht.to_subtype
  rcases (hd.subtype _ _).exists_mem_filter_of_disjoint with ⟨s, hsl, hsd⟩
  lift s to (i : t) → {s // s ∈ l i} using hsl
  rcases @Subtype.exists_pi_extension ι (fun i => { s // s ∈ l i }) _ _ s with ⟨s, rfl⟩
  exact ⟨fun i => s i, fun i => (s i).2, hsd.set_of_subtype _ _⟩

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
⊢ map (eval i) (pi f) = f i

Tactic:
refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
i : ι
s : Set (α i)
hs : s ∈ map (eval i) (pi f)
⊢ s ∈ f i
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
rw [biInter_eq_iInter, biInter_eq_iInter]

Goal state after:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
Set.prod_eq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 (Prod.fst ⁻¹' s ∪ Prod.snd ⁻¹' t) = 𝓟 (Prod.fst ⁻¹' sᶜ ∩ Prod.snd ⁻¹' tᶜ)ᶜ
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case empty
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
n : M₀
h : ∀ a ∈ 0, Prime a
div : ∀ a ∈ 0, a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) 0 ≤ 1
⊢ prod 0 ∣ n

Tactic:
simp only [Multiset.prod_zero, one_dvd]

Goal state after: