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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ star a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))

Tactic:
← mem_star_iff _ a,

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ a ∈ star (Algebra.adjoin R (↑S ⊔ ↑(star S)))
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd

Goal state after:
case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
⊢ x ∈ periodicPts f

Tactic:
obtain ⟨m, n, heq, hne⟩ : ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n := by
    simpa [Injective] using not_injective_infinite_finite (f^[·] x)

Goal state after:
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
m n : ℕ
heq : f^[m] x = f^[n] x
hne : m ≠ n
⊢ x ∈ periodicPts f
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).dropLast ++ [(y :: l).getLast ⋯]).nextOr x y = y

Tactic:
hx,

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).dropLast ++ [(y :: l).getLast ⋯]).nextOr ((y :: l).getLast ⋯) y = y
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

Tactic:
exact IH hx.right

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d] <:+: l

Tactic:
refine infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩
  · have ⟨_, _⟩ := l.dropLast_prefix
    grind
  by_cases hi₁ : i = 1
  · grind [next, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
  · grind [getElem?_idxOf, mem_of_mem_dropLast]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.next l[k] hx = l'.next l[k] ⋯

Tactic:
obtain ⟨n, rfl⟩ := id h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l.next l[k] hx = (l.rotate n).next l[k] ⋯
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ q = ↑(g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q)

Tactic:
← smul_eq_mul,

Goal state after:
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ q = ↑(g ^ minimalPeriod (fun x ↦ g • x) q • Quotient.out q)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.primeFactorsList = [p]

Tactic:
have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl

Goal state after:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.primeFactorsList = [p]
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b.primeFactorsList.prod = a * b

Tactic:
prod_primeFactorsList hb

Goal state after:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b = a * b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
this : Subsingleton (MulAction.orbitRel.Quotient G X)
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

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

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case refine_2
m n : ℕ
hn : n ≠ 0
⊢ (∃ k > 1, n = m * k) → m ∈ n.properDivisors

Tactic:
rintro ⟨k, hk, rfl⟩
    rw [mul_ne_zero_iff] at hn
    exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
simp [hsub]

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

Tactic:
hx,

Goal state after:
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, (-1) ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ ∀ m < n, m ∣ n → m = 1

Tactic:
intro m hm hdvd

Goal state after:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
hdvd : m ∣ n
⊢ m = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ∀ (hm : n ≠ 0), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
intro hn

Goal state after:
case succ.succ.ind
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.cons
b hd₁ hd₂ : ℕ
tl₂ : List ℕ
ih₂ :
  ∀ (tl₁ : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁.length = l2.length →
          ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)) →
      (hd₁ :: tl₁).length = tl₂.length →
        ofDigits b (hd₁ :: tl₁) + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) tl₂)
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = (hd₂ :: tl₂).length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
    ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))

Tactic:
simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]

Goal state after:
case cons.cons
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁_1.length = l2.length →
          ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁_1 l2)) →
      tl₁.length = tl₁_1.length + 1 →
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
    hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ tl₂)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1

Tactic:
digits_zero_succ,

Goal state after:
case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ [n + 1].sum ≤ n + 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
by
  by_cases hf : FiniteMultiplicity a b
  · rw [← ENat.natCast_zero, emultiplicity_eq_coe]
    simp
  · simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
by
  obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b
  refine ⟨c, hc, ?_⟩
  rintro ⟨k, hk⟩
  rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc
  have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩
  exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1

Tactic:
intro n hn_pos hnx

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0

Tactic:
rwa [orderOf, minimalPeriod, dif_neg]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ L ≠ []

Tactic:
simp [ne_nil_iff_length_pos, hL₁]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ x ^ (2 * r + 1) * x = x

Tactic:
hx,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
h2 : 2 * (r + 1) = 2 * r + 1 + 1
⊢ 1 * x = x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
key : x ^ (2 * (r + 1)) = x
⊢ x ^ n = (x ^ (2 * (r + 1))) ^ n

Tactic:
key

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
key : x ^ (2 * (r + 1)) = x
⊢ x ^ n = x ^ n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ ↑(multiplicity p (a * b)) = ↑(multiplicity p a) + emultiplicity p b

Tactic:
hfin.mul_right.emultiplicity_eq_multiplicity

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ ↑(multiplicity p (a * b)) = ↑(multiplicity p a) + ↑(multiplicity p b)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n

Tactic:
· rintro (n_eq_zero | not_dvd)
    · simp [n_eq_zero]
    · simp [Nat.factorization_eq_zero_of_not_dvd not_dvd]

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 * x ^ k = x ^ m * 1 ↔ m + k ≡ m [MOD orderOf x]

Tactic:
mul_left_cancel_iff,

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p - 1) * multiplicity p n ! = n - (p.digits n).sum

Tactic:
by
  simp only [multiplicity_eq_of_emultiplicity_eq_some <|
      emultiplicity_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
    ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
    sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

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

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

Tactic:
by
  have hp' := hp.prime
  have h0 : 2 ≤ p := hp.two_le
  have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
  have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
  have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
  have hm : emultiplicity p (p * n)! ≠ ⊤ := by
    rw [Ne, emultiplicity_eq_top, Classical.not_not, Nat.finiteMultiplicity_iff]
    exact ⟨hp.ne_one, factorial_pos _⟩
  revert hm
  have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0 := by
    intro m hm
    rw [emultiplicity_eq_zero, not_dvd_iff_lt_mul_succ _ hp.pos]
    rw [mem_Ico] at hm
    exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
  simp_rw [← prod_Ico_id_eq_factorial, Finset.emultiplicity_prod hp', ← sum_Ico_consecutive _ h1 h3,
    add_assoc]
  intro h
  rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
← zpow_one x

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ k.primeFactors

Tactic:
← Nat.primeFactors_pow k hn,

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ (k ^ n).primeFactors
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (X ^ (n✝ + 1)).divX = if n✝ + 1 = 0 then 0 else X ^ (n✝ + 1 - 1)

Tactic:
ext n
    simp [coeff_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f✝ f g : R[X]
ihf : (expand R 1) f = f
ihg : (expand R 1) g = g
⊢ (expand R 1) (f + g) = f + g

Tactic:
by rw [map_add, ihf, ihg]

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

Goal state before:
pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ n / p ∉ f.support → (if p * (n / p) = n then f.coeff (n / p) else 0) = 0

Tactic:
intro hn

Goal state after:
case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then f.coeff (n / p) else 0) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
intro _ H

Goal state after:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)

Tactic:
rw [derivative_apply]
  simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
  rw [sum, Finset.sum_eq_single (n + 1)]
  · simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]; norm_cast
  · intro b
    cases b
    · intros
      rw [Nat.cast_zero, mul_zero, zero_mul]
    · intro _ H
      rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
  · simp_all

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

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

Tactic:
intro hn

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 0 = f.coeff (n * p)
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
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
cancelLeads,

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 * X ^ (p.natDegree - q.natDegree) * q -
        C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p).natDegree <
    q.natDegree
Module: Mathlib.Algebra.Polynomial.Div

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

Tactic:
cases degree (p %ₘ (X - C a))

Goal state after:
case bot
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ ⊥ < 1 → ⊥ ≤ 0

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
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p

Tactic:
hx,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x p - 0 * eval₂ f x (p /ₘ q) = eval₂ f x p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
⊢ p = q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hpq : p ∣ 0
h₁ : natDegree 0 ≤ p.natDegree
h₂ : p.leadingCoeff = leadingCoeff 0
⊢ p = 0

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ comap Prod.fst f ⊓ ⊤ = comap Prod.fst f

Tactic:
inf_top_eq

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
⊢ comap Prod.fst f = comap Prod.fst f
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ a ⊓ ⊤ = ∂ a

Tactic:
inf_top_eq

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ a = ∂ a
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ a ⊓ ⊤ = a

Tactic:
inf_top_eq

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ a = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (fun x ↦ x) (normalizedFactors (x * y)) =
    Multiset.map (fun x ↦ x) (normalizedFactors x) + normalizedFactors y

Tactic:
←
    Multiset.map_id' (normalizedFactors y),

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (fun x ↦ x) (normalizedFactors (x * y)) =
    Multiset.map (fun x ↦ x) (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Tactic:
UniqueFactorizationMonoid.normalizedFactors_pow,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ k • normalizedFactors p = Multiset.replicate k (normalize p)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ a * b

Tactic:
hx,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ p * x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
hη₁ : η₁ ∈ nthRootsFinset n a₁
hη₂ : η₂ ∈ nthRootsFinset n a₂
⊢ η₁ * η₂ ∈ nthRootsFinset n (a₁ * a₂)

Tactic:
cases n with
  | zero =>
    simp only [nthRootsFinset_zero, notMem_empty] at hη₁
  | succ n =>
    rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢
    rw [mul_pow, hη₁, hη₂]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x = 0
⊢ y = 0

Tactic:
hx,

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : 0 ∣ y
hx : x = 0
⊢ y = 0