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

Goal state before:
pp: case mem.algebraMap
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 : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
r✝ : R
⊢ p ((algebraMap R A) r✝) z ⋯ ⋯

Tactic:
| algebraMap _ =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.algebraMap
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 : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r r✝ : R
⊢ p ((algebraMap R A) r✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
| algebraMap _ =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b : A
r✝ : R
⊢ p ⟨(Algebra.algebraMap R A) r✝, ⋯⟩

Tactic:
| algebraMap _ =>

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Fintype α
⊢ Injective f ↔ f^[(card α)!] = id

Tactic:
simp only [injective_iff_periodicPts_eq_univ, mem_periodicPts_iff_isPeriodicPt_factorial_card,
    funext_iff, eq_univ_iff_forall, IsPeriodicPt, id, IsFixedPt]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) ((x :: y :: l) :: map (cons y) (permutations'Aux x l)) =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1

Tactic:
count_cons_self

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
y : α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: y :: l) (map (cons y) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (y :: l)).length + 1
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
h : ∀ (m : M), m • a = a
m p : M
⊢ (fun m ↦ m • a) m = (fun m ↦ m • a) p

Tactic:
simp only [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.prev hs x hx ∈ s

Tactic:
rw [← next_reverse_eq_prev, ← mem_reverse_iff]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ¬IsPrimePow 0

Tactic:
by
  simp only [isPrimePow_def, not_exists, not_and', and_imp]
  intro x n _hn hx
  rw [eq_zero_of_pow_eq_zero hx]
  simp

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

Goal state before:
pp: case mp.cons
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
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
prod_cons

Goal state after:
case mp.cons
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
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
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 ∣ (a :: l₁).prod

Tactic:
prod_cons

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
⊢ a ∣ a * l₁.prod
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ n.primeFactorsList

Tactic:
by
  refine perm_of_prod_eq_prod ?_ ?_ ?_
  · rw [h₁]
    refine (prod_primeFactorsList ?_).symm
    rintro rfl
    rw [prod_eq_zero_iff] at h₁
    exact Prime.ne_zero (h₂ 0 h₁) rfl
  · simp_rw [← prime_iff]
    exact h₂
  · simp_rw [← prime_iff]
    exact fun p => prime_of_mem_primeFactorsList

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

Goal state before:
pp: k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList

Tactic:
exact (sublist_append_left _ _).subperm

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ K.index * (H.subgroupOf K).index = H.index

Tactic:
index,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ Nat.card (G ⧸ K) * Nat.card (↥K ⧸ H.subgroupOf K) = Nat.card (G ⧸ H)
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
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index

Tactic:
index,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card (G ⧸ H) * Nat.card (G' ⧸ K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ (pi Set.univ H).index = ∏ i, (H i).index

Tactic:
index,

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
⊢ Nat.card ((ι → G) ⧸ pi Set.univ H) = ∏ i, Nat.card (G ⧸ H i)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #(filter ((fun g ↦ f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) univ) =
    #{g | f g = f ((fun x_1 ↦ x * x_1) y)}

Tactic:
congr 2 with g

Goal state after:
case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
⊢ ((fun g ↦ f g = f x) ∘ ⇑(Equiv.toEmbedding (Equiv.mulRight y⁻¹))) g ↔ f g = f ((fun x_1 ↦ x * x_1) y)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g * ↑(f'.toHomUnits y)⁻¹ = f' x ↔ f' g = f' x * f' y

Tactic:
Units.mul_inv_eq_iff_eq_mul,

Goal state after:
case e_p
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y g : G
f' : G →* M := ↑f
⊢ f' g = f' x * ↑(f'.toHomUnits y) ↔ f' g = f' x * f' y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ a.val + b.val = (a + b).val + n

Tactic:
by
  rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
    Nat.mod_eq_of_lt (val_lt _)]
  rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
rw [← properDivisors_eq_singleton_one_iff_prime]

Goal state after:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ n / (p * p) < n / p

Tactic:
rw [← Nat.dvd_iff_mod_eq_zero] at hmod

Goal state after:
n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : p ∣ n
⊢ n / (p * p) < n / p
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hlt : a < k
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd
    exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd

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

Goal state before:
pp: case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
exact pow_dvd_iff_le_of_spec hp₁ hn (pow_padicValNat_mul_divMaxPow p n)
      (not_dvd_divMaxPow hp₁ hn)

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

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
by
  by_cases h : n = 0
  · have : 0 < b ^ k := by positivity
    simpa [h]
  rw [length_digits b n hb h, ← log_lt_iff_lt_pow hb h]
  exact add_one_le_iff

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
rw [← List.dropLast_append_getLast hl]
  simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append,
    List.length_dropLast, ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
  apply Nat.mul_le_mul_left
  refine le_trans ?_ (Nat.le_add_left _ _)
  have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
  convert! Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
  rw [Nat.mul_one]

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

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

Tactic:
(intro n c tl; 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:
(intro n c tl; simp only [Nat.toDigitsCore, List.length])

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
constructor
  · intro h
    constructor
    · apply pow_dvd_of_le_emultiplicity
      simp [h]
    · apply not_pow_dvd_of_emultiplicity_lt
      rw [h]
      norm_cast
      simp
  · rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

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

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l d : ℕ
hd₁ : d < b
T : List ℕ
hT : T ∈ fixedLengthDigits hb l
⊢ d :: T ∈ fixedLengthDigits hb (l + 1)

Tactic:
exact cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∀ a ∈ List.fixedLengthDigits hb l, ofDigits b a ∈ Finset.range (b ^ l)

Tactic:
by exact (bijOn_ofDigits' hb l).1

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Subsingleton Gˣ
x : G
h : IsUnit x
⊢ orderOf x = 1

Tactic:
by
  simp [isUnit_iff_eq_one.mp h]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf (x ^ n) = orderOf x / n

Tactic:
orderOf_pow' _ hn,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf x / (orderOf x).gcd n = orderOf x / n
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Goal state after:
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Goal state after:
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p

case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k

Tactic:
by
  conv_rhs => rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]
  rw [eq_comm]
  apply Finset.prod_subset
  · intro p hp
    rw [Finset.mem_range]
    contrapose! hp
    rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
  · intro p _ h2
    simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x)) = x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x)))

Tactic:
by
        simp [zpow_add, zpow_mul, pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm y ^ k) a = a

Tactic:
exact Function.IsFixedPt.perm_zpow (by exact hs) k

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

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

Tactic:
rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑g ^ H.index = 1

Tactic:
index,

Goal state after:
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑g ^ Nat.card (G ⧸ H) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
symm at h

Goal state after:
case pos
a b m n : ℕ
hmn : m.Coprime n
h : b ^ n = a ^ m
ha0 : a = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ g • a = a

Tactic:
have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))
  rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
  exact le_antisymm key h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
⊢ a ^ (n + 1) ∈ S

Tactic:
by
    induction n with
    | zero => rwa [zero_add, pow_one]
    | succ n ih =>
      rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
⊢ (expand R 0) f = C (eval 1 f)

Tactic:
simp [expand]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p

Tactic:
mul_smul_comm,

Goal state after:
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : eval x (p /ₘ (X - C x) ^ rootMultiplicity x p) * eval x (q /ₘ (X - C x) ^ rootMultiplicity x q) ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
simp_rw [eval_divByMonic_eq_trailingCoeff_comp] at hpq
  simp_rw [rootMultiplicity_eq_natTrailingDegree, mul_comp, natTrailingDegree_mul' hpq]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
⊢ p.degree = q.degree

Tactic:
by
  let ⟨u, hu⟩ := h
  simp [hu.symm]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p a * f + contract p b * g = 1

Tactic:
simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ (aeval x) (map (algebraMap R A) p) = (aeval x) p

Tactic:
aeval_def,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x) p
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ (algebraMap A B) x (map (algebraMap R A) p) = (aeval x) p

Tactic:
aeval_def,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ (algebraMap A B) x (map (algebraMap R A) p) = eval₂ (algebraMap R B) x p
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ (aeval ((algebraMap A B) x)) p = (algebraMap A B) ((aeval x) p)

Tactic:
aeval_def,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = (algebraMap A B) ((aeval x) p)
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = (algebraMap A B) ((aeval x) p)

Tactic:
aeval_def,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = (algebraMap A B) (eval₂ (algebraMap R A) x p)