mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
erase_ne hqp

Goal state after:
case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ a.factorization q ≤ b.factorization q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  ext x
  simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
    pp.pow_dvd_iff_le_factorization hn, iff_and_self]
  exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)

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
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.divX = 0
⊢ p = C (p.coeff 0)

Tactic:
by simpa [eq_comm, h] using divX_mul_X_add p

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
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
key : g ^ ↑((Nat.card G).gcd n) = g ^ (↑(Nat.card G) * (Nat.card G).gcdA n + ↑n * (Nat.card G).gcdB n)
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
o : ℕ
p : R[X]
coeff_ne_zero : p.coeff o ≠ 0
h_natDeg_le : p.natDegree ≤ o
⊢ p.natDegree = o

Tactic:
exact natDegree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ trailingDegree 0 = trailingDegree 0 + q.trailingDegree

Tactic:
trailingDegree_zero,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ ⊤ = ⊤ + q.trailingDegree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ trailingDegree 0 = p.trailingDegree + trailingDegree 0

Tactic:
trailingDegree_zero,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ ⊤ = p.trailingDegree + ⊤
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree →
    (if q.degree ≤ p.degree ∧ ¬p = 0 then
            (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
                ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
          else (0, p)).2.degree <
      q.degree

Tactic:
if_neg h

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ¬q.degree ≤ p.degree → (0, p).2.degree < q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff

Tactic:
by
      simp [mul_comm]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
⊢ y ∈ ↑(antidiagonal n) → (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y → x = y

Tactic:
hy

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ ↑(antidiagonal n)
y : ℕ × ℕ
hy : y ∈ ↑(antidiagonal n)
⊢ (fun x ↦ (x.1 * p, x.2 * p)) x = (fun x ↦ (x.1 * p, x.2 * p)) y → x = y
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ False

Tactic:
apply hfg

Goal state after:
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ f /ₘ g = 0
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 + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ ((X - C a) ^ if p = 0 then 0 else multiplicity (X - C a) p) ∣ p

Tactic:
if_neg h

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U

case mpr
α : Type u
s : Set (Set α)
U : Set α
h : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) = 0

Tactic:
← IsRoot,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬(p /ₘ (X - C a) ^ rootMultiplicity a p).IsRoot a
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: α : Type u_2
β : Type u_3
f : Filter α
g : Filter β
⊢ (f ×ˢ g).ker = f.ker ×ˢ g.ker

Tactic:
by
  simp [Set.prod_eq, Filter.prod_eq_inf]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
refine exists_congr fun i => ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∈ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp [hi, NeBot.ne']

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
i : ι
hi : i ∉ I
⊢ f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥ ↔ i ∈ I ∧ f i ⊓ 𝓟 (s i) = ⊥

Tactic:
simp [hi, NeBot.ne']

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤

Tactic:
by
    rintro ⟨b, rfl⟩
    exact hnot_boundary _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map (fun p ↦ (f p.1, g p.2)) (a ×ˢ b) ≤ c ×ˢ d

Tactic:
← prod_map_map_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : α → β
a : α
b : β
⊢ update f a b =ᶠ[𝓟 {a}ᶜ] f

Tactic:
filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _

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

Goal state before:
pp: case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ f i * (Multiset.map f (s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)

Tactic:
← Multiset.prod_cons,

Goal state after:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
j : ι
hj : j ∈ s
⊢ (f i ::ₘ Multiset.map f (s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g

Tactic:
rw [← Multiset.cons_erase hbg]

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ g.erase b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p * f.prod ~ᵤ b * (g.erase b).prod

Tactic:
← Multiset.prod_cons,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ (p ::ₘ f).prod ~ᵤ b * (g.erase b).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ (p ::ₘ f).prod ~ᵤ b * (g.erase b).prod

Tactic:
← Multiset.prod_cons,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ (p ::ₘ f).prod ~ᵤ (b ::ₘ g.erase b).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * (q * (s.erase q).prod)

Tactic:
← Multiset.prod_cons,

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * (q ::ₘ s.erase q).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count (f x) (Multiset.map f (p.comp (C a * X + C b)).roots) = count (f x) p.roots

Tactic:
rw [count_roots, count_map_eq_count' f _ hf.injective, count_roots,
    rootMultiplicity_comp_C_mul_X_add_C p a b x ha]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map normalize s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ b ∈ s, Irreducible b
b : α
hb : b ∈ s
this : Nontrivial α
⊢ normalizedFactors (a * s.prod) = normalize a ::ₘ Multiset.map normalize s

Tactic:
normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),

Goal state after:
case cons.inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : (∀ a ∈ s, Irreducible a) → normalizedFactors s.prod = Multiset.map normalize s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ b ∈ s, Irreducible b
b : α
hb : b ∈ s
this : Nontrivial α
⊢ normalizedFactors a + normalizedFactors s.prod = normalize a ::ₘ Multiset.map normalize s
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s : Set α
this :
  ∀ (s : Set (α →₀ ℕ)),
    ((fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' (n • s)
⊢ (f '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' {x | degree x = n ∧ ↑x.support ⊆ s}

Tactic:
simp [← nsmul_single_one_image, ← this, Set.image_image]

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
hη : 0 ∈ nthRootsFinset 0 a
⊢ False

Tactic:
simp only [nthRootsFinset_zero, notMem_empty] at hη

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ∀ x ∈ p.support, p.coeff x = 0
⊢ p = 0

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ x ∈ p.support, p.coeff x = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p

Tactic:
refine ⟨fun h => ?_, Prime.irreducible⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime 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
⊢ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
convert! eif using 7

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
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
⊢ f = 0

Tactic:
have := Fintype.ofFinite R

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
p q : R[X]
⊢ (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)

Tactic:
hpq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
p q : R[X]
hpq : (p * q).degree < ↑n
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝¹, Irreducible a

Tactic:
intro a ha
        obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
        rwa [Subtype.coe_mk]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝, Irreducible a

Tactic:
intro a ha
        obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
        rwa [Subtype.coe_mk]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p

Tactic:
by
  classical
  have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 ↦ absurd hp1 (by simp [hp0]))
  exact (normalize_associated _).prime this

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)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
pp : p = ⟨↑p, ⋯⟩
⊢ k ∣ Multiset.count ⟨↑p, ⋯⟩ (factors' a0)

Tactic:
← count_some p.2

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
p : { a // Irreducible a }
pp : p = ⟨↑p, ⋯⟩
⊢ k ∣ (↑p).count ↑(factors' a0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
⊢ IsAlgebraic (↥B) x

Tactic:
let : Algebra A B := (Subalgebra.inclusion hle).toAlgebra

Goal state after:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
⊢ IsAlgebraic (↥B) x
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f j) y = w

Tactic:
hy

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
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
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ w = w
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit piLTProj i)
⊢ (fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) t) = t

Tactic:
by ext1; ext1; apply Equiv.right_inv

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
z : Q ⊗[R] P
⊢ ∃ a, (lTensor Q g) a = z

Tactic:
induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul q p =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨q ⊗ₜ[R] n, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

Goal state after: