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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (p.factorization p + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
hp.factorization_self,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (1 + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
by
  rcases em' p.Prime with (pp | pp); · simp [pp]
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rw [pow_dvd_pow_iff_le_right pp.one_lt]
  exact (factorization_le_iff_dvd ha0 hb0).2 hab p

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

Goal state before:
pp: case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

pp: case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
· lia

Goal state after:
case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n ≡ m [MOD 0]
⊢ n = m

Tactic:
modEq_zero_iff

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : n = m
⊢ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ n ≡ m [MOD 0] ↔ n = m

Tactic:
modEq_zero_iff

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ n = m ↔ n = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a = b

Tactic:
← div_eq_one

Goal state after:
G : Type u_1
inst✝ : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : (fun a ↦ a ^ n) a / (fun a ↦ a ^ n) b = 1
⊢ a / b = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case zero
n : ℕ
⊢ #({k ∈ Finset.range (succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n

Tactic:
simp [Finset.filter_false_of_mem]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
R : Type u_6
inst✝¹ : NonAssocRing R
p : ℕ
inst✝ : Fintype R
hn : card R = p
hR : ∀ i < p, ↑i = 0 → i = 0
H : ↑p = 0
n : ℕ
⊢ ↑(p * n) = 0

Tactic:
rw [Nat.cast_mul, H, zero_mul]

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
h_mul_left : f.natDegree ≤ df
h_mul_right : g.natDegree ≤ dg
ddf : df + dg ≤ df + dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
exact coeff_mul_add_eq_of_natDegree_le ‹_› ‹_›

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ (expand R p) f = C r ↔ f = C r

Tactic:
rw [← expand_C, expand_inj hp, expand_C]

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

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).coeff (f.natDegree * p) ≠ 0

Tactic:
coeff_expand_mul hp,

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ f.coeff f.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ ((expand R p) f).natDegree = f.natDegree * p

Tactic:
by
  rcases p.eq_zero_or_pos with hp | hp
  · rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
  by_cases hf : f = 0
  · rw [hf, map_zero, natDegree_zero, zero_mul]
  have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]
  refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
  · rw [coeff_expand hp]
    split_ifs with hpn
    · rw [coeff_eq_zero_of_natDegree_lt]
      contrapose! hn
      norm_cast
      rw [← Nat.div_mul_cancel hpn]
      exact Nat.mul_le_mul_right p hn
    · rfl
  · refine le_degree_of_ne_zero ?_
    rw [coeff_expand_mul hp, ← leadingCoeff]
    exact mt leadingCoeff_eq_zero.1 hf

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).Monic ↔ f.Monic

Tactic:
by
  simp only [Monic, leadingCoeff_expand hp]

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:
let ⟨u, hu⟩ := h
  simp [hu.symm]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ 0 %ₘ q = 0

Tactic:
zero_modByMonic

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ 0 = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩

Goal state after:
case refine_1
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i : ι
⊢ (fun i ↦ ⋂ j, ↑s ∩ ↑t) i ∈ l i

case refine_2
α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
s : ⦃i : ι⦄ → ⦃j : ι⦄ → { s // s ∈ l i }
t : ⦃i : ι⦄ → ⦃j : ι⦄ → { t // t ∈ l j }
hst : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ↑s ↑t
i j : ι
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⋂ j, ↑s ∩ ↑t) i j
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

Tactic:
by
  rw [le_rootMultiplicity_iff hzero]
  exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

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

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂

Tactic:
by rw [coprod_eq_prod_top_sup_top_prod]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ (map (fun x ↦ b) (𝓟 {a})).coprod (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})

Tactic:
by
  simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
    prod_univ, univ_prod, id]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i

Tactic:
induction s using Finset.induction with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case empty
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : Multiset.prod 0 = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
apply subset_closure

Goal state after:
case empty
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : Multiset.prod 0 = x * y
⊢ x ∈ {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
⊢ b ∣ k

Tactic:
have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)

Goal state after:
case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
⊢ b ∣ k
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (X - C r).roots = {r}

Tactic:
classical
  ext s
  rw [count_roots, rootMultiplicity_X_sub_C, count_singleton]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
List.prod_cons,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd * tl.prod).roots = (↑(hd :: tl)).bind roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : Multiset R[X]
L : List R[X]
⊢ 0 ∉ Quot.mk (⇑(List.isSetoid R[X])) L →
    (prod (Quot.mk (⇑(List.isSetoid R[X])) L)).roots = Multiset.bind (Quot.mk (⇑(List.isSetoid R[X])) L) roots

Tactic:
simpa only [Multiset.prod_coe, quot_mk_to_coe''] using! roots_list_prod L

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 1 = 0

Tactic:
nontriviality α using factors
  rw [← rel_zero_right]
  refine factors_unique irreducible_of_factor (fun x hx => (notMem_zero x hx).elim) ?_
  rw [prod_zero]
  exact factors_prod one_ne_zero

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0

Tactic:
by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

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

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
⊢ q ∣ p * a' → q ∣ b' → IsUnit q

Tactic:
q_dvd_pa'

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
⊢ q ∣ b' → IsUnit q
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ p ∣ s ∧ q ∣ s → r ∣ s

Tactic:
suffices hs : ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s from
      hs s.natDegree s rfl

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
← p.roots.card_map f

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ (Multiset.map (⇑f) p.roots).card ≤ (map f p).roots.card
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ (s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S

Tactic:
by
  classical
  simp only [rootSet, aroots, ← Finset.mem_coe]
  rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
  rwa [← Polynomial.map_prod, Ne, Polynomial.map_eq_zero]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff⁻¹ = p.leadingCoeff / q.leadingCoeff

pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Tactic:
div_eq_mul_inv

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff⁻¹ = p.leadingCoeff * q.leadingCoeff⁻¹

R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a b : R
inst✝ : Field R
⊢ C (a / b) = C (a * b⁻¹)

Tactic:
div_eq_mul_inv

Goal state after:
R : Type u
a b : R
inst✝ : Field R
⊢ C (a * b⁻¹) = C (a * b⁻¹)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

Tactic:
count_mul ha hb hp

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.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
x : A
⊢ Function.Injective ⇑(aeval x) ↔ RingHom.ker (aeval x) = ⊥

Tactic:
RingHom.injective_iff_ker_eq_bot

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ RingHom.ker (aeval x) = ⊥ ↔ RingHom.ker (aeval x) = ⊥
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * s ^ rootMultiplicity 0 p = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
exact ⟨q, hq, (S⁰.pow_mem hs (rootMultiplicity 0 p)).2 (aeval s q) hp⟩

Goal state after:
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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g✝¹ : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) ((f i j hij) x) = (g✝¹ i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g✝ : (i : ι) → G i →ₗ[R] G' i
hg : ∀ (i j : ι) (h : i ≤ j), g✝ j ∘ₗ f i j h = f' i j h ∘ₗ g✝ i
i j : ι
h : i ≤ j
g : G i
⊢ (of R ι G' f' j ∘ₗ g✝ j) ((f i j h) g) = (of R ι G' f' i ∘ₗ g✝ i) g

Tactic:
have eq1 := LinearMap.congr_fun (hg i j h) g

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 ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g✝¹ : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) ((f i j hij) x) = (g✝¹ i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g✝ : (i : ι) → G i →ₗ[R] G' i
hg : ∀ (i j : ι) (h : i ≤ j), g✝ j ∘ₗ f i j h = f' i j h ∘ₗ g✝ i
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j ∘ₗ f i j h) g = (f' i j h ∘ₗ g✝ i) g
⊢ (of R ι G' f' j ∘ₗ g✝ j) ((f i j h) g) = (of R ι G' f' i ∘ₗ g✝ i) g
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ (e₁ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩ = (e₂ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩

Tactic:
piLTProj_intro (f := e₁ _ x) (le_succ i) (by exact hj),

Goal state after:
case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ piLTProj ⋯ ((e₁ ⟨i⁺, hi✝⟩) x) ⟨↑⟨j, hj✝⟩, hj⟩ = (e₂ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.tmul.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0

Tactic:
use 0
          simp only [map_zero, smul_eq_mul, mul_zero]

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

Goal state before:
pp: case a.refine_4.tmul.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
a : A
b : B
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0

Tactic:
use 0
          simp only [map_zero, smul_eq_mul, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddMonoid (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarAddMonoid (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝¹⟩⟧ + star ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [add_def, star_def, star_add, add_def]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b + 1 - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x ≤ b

pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x

Tactic:
· lia

Goal state after:
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x ≤ b → ∃ a_2 < (b + 1 - a).toNat, a + ↑a_2 = x
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case mp
a b x : ℤ
⊢ (∃ a_1 < (b - a).toNat, a + ↑a_1 = x) → a ≤ x ∧ x < b

pp: case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x

Tactic:
· lia

Goal state after:
case mpr
a b x : ℤ
⊢ a ≤ x ∧ x < b → ∃ a_2 < (b - a).toNat, a + ↑a_2 = x