mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: List.replicate k 0 ++ b.digits m

Tactic:
List.cons_append

Goal state after:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: (List.replicate k 0 ++ b.digits m)
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 = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ x ∈ Ico 0 tl.length, ofDigits p (List.drop (1 + x) tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
Ico_zero_eq_range,

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
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) *
      (∑ k ∈ range 1, ofDigits p (List.drop k tl) + ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) +
        ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ multiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
simp [multiplicity_eq_zero]

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
⊢ ¬IsOfFinOrder x

Tactic:
isOfFinOrder_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬∃ n, 0 < n ∧ x ^ n = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝ : ℕ
h : x✝ ∈ {n | n < b ^ l}
⊢ (b.digitsAppend l x✝).length = l

Tactic:
length_digitsAppend hb _ h

Goal state after:
b : ℕ
hb : 1 < b
l x✝ : ℕ
h : x✝ ∈ {n | n < b ^ l}
⊢ l = l
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ IsOfFinOrder ↑x ↔ IsOfFinOrder x

Tactic:
isOfFinOrder_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ (∃ n, 0 < n ∧ ↑x ^ n = 1) ↔ IsOfFinOrder x
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ ¬IsOfFinOrder x ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
isOfFinOrder_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ (¬∃ n, 0 < n ∧ x ^ n = 1) ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Tactic:
exact Nat.pos_of_dvd_of_pos h hx

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

Goal state before:
pp: n p : ℕ
hp : Prime p
q : ℕ
⊢ q ∈ replicate (count p n.primeFactorsList) p →
    count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList

Tactic:
hq

Goal state after:
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
by
  by_cases h : (choose n k).factorization p = 0
  · simp [h]
  have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_not_prime h
  have hkn : k ≤ n := by
    refine le_of_not_gt fun hnk => h ?_
    simp [choose_eq_zero_of_lt hnk]
  rw [factorization_choose hp hkn (Nat.lt_add_one _)]
  exact (card_filter_le ..).trans_eq (Nat.card_Ico _ _)

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

Goal state before:
pp: p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ emultiplicity p 0! = ↑(∑ i ∈ Ico 1 b, 0 / p ^ i)

Tactic:
simp [Ico, hp.emultiplicity_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid ≤ Submonoid.closure s

Tactic:
rw [closure_toSubmonoid]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ Submonoid.closure (s ∪ s⁻¹) ≤ Submonoid.closure s
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0

Tactic:
simpa only [one_mul] using mul_of'_modOf (1 : k[G]) g

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
inst✝¹ : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst✝ : Finite ι
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
by
  have := Fintype.ofFinite ι
  simp only [← orderOf_ne_zero_iff, Pi.orderOf]
  simp [Finset.lcm_eq_zero_iff]

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

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

Tactic:
derivative_eval₂_C,

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ derivative (map f p) = map f (derivative p)

Tactic:
let n := max p.natDegree (map f p).natDegree

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ derivative (map f p) = map f (derivative p)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n) * r + q ^ n * derivative r

Tactic:
derivative_pow

Goal state after:
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ C ↑n * q ^ (n - 1) * derivative q * r + q ^ n * derivative r
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a

Tactic:
simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)

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

Goal state before:
pp: α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

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

Goal state before:
pp: case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Tactic:
rw [← iInf_plift_down, ← iInter_plift_down]

Goal state after:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i.down) = 𝓟 (⋂ i, f i.down)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr✝ : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
a✝ : α
hp : p a✝
⊢ q (y a✝) → r a✝ (y a✝)

Tactic:
hq

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
y : α → β
r : α → β → Prop
hy : Tendsto y f g
hr✝ : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2
p : α → Prop
hp✝ : ∀ᶠ (x : α) in f, p x
q : β → Prop
hq✝ : ∀ᶠ (y : β) in g, q y
hr : ∀ {x : α}, p x → ∀ {y : β}, q y → r (x, y).1 (x, y).2
a✝ : α
hp : p a✝
hq : q (y a✝)
⊢ r a✝ (y a✝)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b

Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α → Prop
q : β → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
Filter.coprod,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ comap Prod.fst (𝓟 s) ⊔ comap Prod.snd (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree x

Tactic:
← hy,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree (mapDomain f y)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
⊢ q ∈ normalizedFactors a → p ∣ q → p = q

Tactic:
hq

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
⊢ p ∣ q → p = q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
⊢ (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a) →
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
      (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
        map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
hs

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
⊢ (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
    (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
      map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : ↑(rootMultiplicity t p) ∈ nonZeroDivisors R
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
by
  by_cases h : p = 0
  · simp only [h, map_zero, rootMultiplicity_zero]
  obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t
  set m := p.rootMultiplicity t
  have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
  have hndvd : ¬(X - C t) ^ m ∣ derivative p := by
    rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
    rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
    rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
  have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
  exact le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
    (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)

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

Goal state before:
pp: case mpr
α : 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
u : Mˣ
hu : (normalizedFactors x).prod * ↑u = x
⊢ (normalizedFactors x, u).1 ≤ normalizedFactors y

Tactic:
exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ a ∣ p.coeff x - q.coeff x

Tactic:
use w.coeff x

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ p.coeff x - q.coeff x = a * w.coeff x
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hdf0 : derivative f ≠ 0
hr : derivative f * 0 = f * r
hg : ¬IsRoot 0 a
⊢ False

Tactic:
simp at hg

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

Goal state before:
pp: case top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
h : prod ⊤ = prod q
⊢ ⊤ = q

Tactic:
induction q

Goal state after:
case top.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
h : prod ⊤ = prod ⊤
⊢ ⊤ = ⊤

case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
q : WithTop (Multiset { a // Irreducible a })
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod q
⊢ ↑a✝ = q

Tactic:
induction q

Goal state after:
case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ ↑a✝ = ⊤

case coe.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
p q : R[X]
h : q = 0
⊢ q * p.div q + p.mod q = p

Tactic:
simp only [h, zero_mul, mod, modByMonic_zero, zero_add]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ (p * r).content ∧ p.primPart ∣ (p * r).primPart

Tactic:
(associated_content_mul ..).dvd_iff_dvd_right,

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ p.content * r.content ∧ p.primPart ∣ (p * r).primPart
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : CommRing K
f : K[X]
a : K
⊢ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Tactic:
by
  have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
  simpa only [derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
    modByMonic_X_sub_C_eq_C_eval] using key

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a))

Tactic:
hu,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * u + (X - C a) * derivative ((X - C a) * u)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q : R[X]
⊢ ∃ c, ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d

Tactic:
by
    rcases exists_primitive_lcm_of_isPrimitive p.isPrimitive_primPart
        q.isPrimitive_primPart with
      ⟨r, rprim, hr⟩
    refine ⟨C (lcm p.content q.content) * r, fun s => ?_⟩
    by_cases hs : s = 0
    · simp [hs]
    by_cases hpq : C (lcm p.content q.content) = 0
    · rw [C_eq_zero, lcm_eq_zero_iff, content_eq_zero_iff, content_eq_zero_iff] at hpq
      rcases hpq with (hpq | hpq) <;> simp [hpq, hs]
    iterate 3 rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]
    nontriviality R
    rw [(associated_content_mul ..).dvd_iff_dvd_left, rprim.content_eq_one, mul_one, content_C,
      (associated_primPart_mul (mul_ne_zero hpq rprim.ne_zero)).dvd_iff_dvd_left, rprim.primPart_eq,
      normalize_lcm, lcm_dvd_iff,
      (isUnit_primPart_C (lcm p.content q.content)).mul_left_dvd, ← hr s.primPart]
    tauto

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
⊢ Irreducible q → q.count a.factors = q.count (p ^ p.count a.factors).factors

Tactic:
hq

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = q.count (p ^ p.count a.factors).factors
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ IsAlgebraic R (?m.24 ↑n)

pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℕ
⊢ R →+* A

Tactic:
exact isAlgebraic_algebraMap (Nat.cast n)

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, ↑f = ↑g ∘ₗ (y • 1)) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
LinearMap.ext_iff,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, ∀ (x : M), ↑f x = (↑g ∘ₗ (y • 1)) x) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a

Tactic:
by
  simp_rw [Transcendental, isAlgebraic_algebraMap_iff h]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) x) =
    (LinearMap.rTensor M (of R ι G f x✝²)) x

Tactic:
refine x.induction_on ?_ ?_ ?_ <;> aesop

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup P'
inst✝² : Module R M'
inst✝¹ : Module R N'
inst✝ : Module R P'
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ (map g g').ker = (lTensor N f').range ⊔ (rTensor N' f).range

Tactic:
rw [← lTensor_comp_rTensor]
  rw [ker_comp]
  rw [← Exact.linearMap_ker_eq (rTensor_exact N' hfg hg)]
  rw [← Submodule.comap_map_eq]
  apply congr_arg₂ _ rfl
  rw [range_eq_map, ← Submodule.map_comp, rTensor_comp_lTensor,
    Submodule.map_top]
  rw [← lTensor_comp_rTensor, range_eq_map, Submodule.map_comp,
    Submodule.map_top]
  rw [range_eq_top.mpr (rTensor_surjective M' hg), Submodule.map_top]
  rw [Exact.linearMap_ker_eq (lTensor_exact P hfg' hg')]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ (F.intervalGapsWithin h a b 0).1 = a

Tactic:
simp [intervalGapsWithin, intervalGapsWithin.fst]

Goal state after: