mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i : Set ι × (ι → κ)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
      ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i' : Set ι × κ),
    i'.1.Finite ∧ p i'.2 →
      ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ i'.1.pi fun i ↦ s i i'.2

Tactic:
· rintro ⟨I, k⟩ ⟨hI, hk⟩
    rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
    exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i' : Set ι × κ),
    i'.1.Finite ∧ p i'.2 →
      ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ i'.1.pi fun i ↦ s i i'.2
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

Tactic:
rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
le_rootMultiplicity_iff h,

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ (X - C 0) ^ p.natTrailingDegree ∣ p
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (comap Prod.fst b ⊓ comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
comap_inf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (comap Prod.fst b) ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd g) ⊓ comap Prod.snd h) =
    comap Prod.fst f ⊓ comap Prod.snd (comap Prod.fst g ⊓ comap Prod.snd h)

Tactic:
comap_inf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.fst (comap Prod.fst f)) ⊓
        comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.fst (comap Prod.snd g)) ⊓
      comap (⇑(Equiv.prodAssoc α β γ).symm) (comap Prod.snd h) =
    comap Prod.fst f ⊓ (comap Prod.snd (comap Prod.fst g) ⊓ comap Prod.snd (comap Prod.snd h))
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.fst f ⊓ comap Prod.snd (comap Prod.fst g ⊓ comap Prod.snd h)) =
    comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd g) ⊓ comap Prod.snd h

Tactic:
comap_inf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.fst f) ⊓
      (comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.snd (comap Prod.fst g)) ⊓
        comap (⇑(Equiv.prodAssoc α β γ)) (comap Prod.snd (comap Prod.snd h))) =
    comap Prod.fst (comap Prod.fst f) ⊓ comap Prod.fst (comap Prod.snd g) ⊓ comap Prod.snd h
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ a ⊓ ⊤ = a
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd g) ⊓ comap Prod.snd (comap Prod.fst h ⊓ comap Prod.snd k)) =
    comap Prod.fst (comap Prod.fst f ⊓ comap Prod.snd h) ⊓ comap Prod.snd (comap Prod.fst g ⊓ comap Prod.snd k)

Tactic:
comap_inf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (comap Prod.fst (comap Prod.fst f)) ⊓
        comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (comap Prod.fst (comap Prod.snd g)) ⊓
      (comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (comap Prod.snd (comap Prod.fst h)) ⊓
        comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (comap Prod.snd (comap Prod.snd k))) =
    comap Prod.fst (comap Prod.fst f) ⊓ comap Prod.fst (comap Prod.snd h) ⊓
      (comap Prod.snd (comap Prod.fst g) ⊓ comap Prod.snd (comap Prod.snd k))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ eval₂ C q (derivative (C r * X ^ n)) * derivative q * q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n) * X + C r * X ^ n * derivative X) * derivative q

Tactic:
derivative_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ eval₂ C q (derivative (C r * X ^ n)) * derivative q * q + eval₂ C q (C r * X ^ n) * derivative q =
    eval₂ C q (derivative (C r * X ^ n) * X + C r * X ^ n * 1) * derivative q
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
⊢ f i * derivative (Multiset.map f s).prod =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
h,

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
⊢ f i * (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ derivative X - derivative (C c) = 1

Tactic:
derivative_X,

Goal state after:
R : Type u
inst✝ : Ring R
c : R
⊢ 1 - derivative (C c) = 1
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
b : β
⊢ (f ⁻¹' {b}).Finite

Tactic:
by simpa using TendstoCofinite.finite_preimage f (by simp)

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
    push _ ∈ _
    simp only [Multiset.prod_zero] at hprod
    left; exact .of_mul_eq_one _ hprod.symm

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
⊢ ∀ {g : Multiset α}, (∀ x ∈ 0, Prime x) → (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
intro g _ hg h

Goal state after:
case empty
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
⊢ Multiset.Rel Associated 0 g
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) f = 0

Tactic:
h,

Goal state after:
case mpr
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) 0 = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : x = 0
⊢ (C x).roots = 0

Tactic:
rw [H, C_0, roots_zero]

Goal state after:
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 normalize (normalizedFactors (x * y)) =
    Multiset.map normalize (normalizedFactors x + normalizedFactors y)

Tactic:
h,

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 (Associates.out ∘ Associates.mk) (normalizedFactors (x * y)) =
    Multiset.map (Associates.out ∘ Associates.mk) (normalizedFactors x + normalizedFactors y)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case zero
σ : Type u_5
f : σ →₀ ℕ
hn : 0 ≤ degree f
⊢ ∃ g ≤ f, degree g = 0

Tactic:
simp [degree_eq_zero_iff]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ (map (⇑Associates.mkMonoidHom ∘ Classical.choose ⋯) (normalizedFactors x)).prod = x

Tactic:
h,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ (map id (normalizedFactors x)).prod = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e (w.prod * ↑u) = a

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e (e.symm a) = a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ p.content = 1

Tactic:
rw [← normalize_content, normalize_eq_one, IsPrimitive]
  simp_rw [← dvd_content_iff_C_dvd]
  exact ⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ nonZeroDivisors R ∧ ↑n ! ∈ nonZeroDivisors R

Tactic:
exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
h,

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t (derivative 0) = rootMultiplicity t 0 - 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = (Multiset.map (fun a ↦ X - C a) p.roots).prod.natDegree + q.natDegree

Tactic:
natDegree_multiset_prod_X_sub_C_eq_card

Goal state after:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.roots.card + q.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
h,

Goal state after:
case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ prod ⊤ = 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 : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * (q.primPart * p.primPart).content))
    (p.content * p.primPart.content * (q.content * q.primPart.content))

Tactic:
h,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * 1)) (p.content * p.primPart.content * (q.content * q.primPart.content))
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ p.degree < q.degree

Tactic:
h,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * 0 + p % q = p
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ Associated (p * q).primPart (p.primPart * q.primPart)

Tactic:
by
  rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0
  refine .of_mul_left ?_ .rfl h0
  conv_lhs => rw [← (p * q).eq_C_content_mul_primPart,
    p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart, mul_mul_mul_comm, ← C_mul]
  gcongr
  exact (associated_content_mul ..).symm.map _

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ∧ Associates.mk a ≤ Associates.mk b

Tactic:
mk_le_mk_iff_dvd,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ Associates.mk a ≤ Associates.mk b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ∧ Associates.mk a ≤ Associates.mk b

Tactic:
mk_le_mk_iff_dvd,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ Associates.mk a ≤ Associates.mk b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case pos
α : 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
h : q = p
⊢ q.count a.factors = p.count a.factors * q.count p.factors

Tactic:
h,

Goal state after:
case pos
α : 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
h : q = p
⊢ p.count a.factors = p.count a.factors * p.count p.factors
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
a b : S
hRb : IsAlgebraic R b
hb : b ∈ S⁰
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ (algebraMap R S) r * a = b * (s * a)

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : b ∈ S⁰
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ b * s * a = b * (s * a)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) p.divX * (aeval x) X + (aeval x) (C (p.coeff 0))

Tactic:
h,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = 0 * (aeval x) X + (aeval x) (C (p.coeff 0))
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
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]

Goal state after:
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
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (lTensor Q f).range.mkQ y
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ 1 ≤ restrictSupport R 0

Tactic:
· rintro _ ⟨x, rfl⟩
    simp [mem_restrictSupport_iff, subset_def, coeff, AddMonoidAlgebra.one_def,
      Finsupp.single_apply]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
P : ι → Submodule R M
inst✝¹ : Small.{u, u_3} ι
inst✝ : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2} ↥(iSup P)

Tactic:
rw [iSup_eq_range_dfinsupp_lsum]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type u_3
P : ι → Submodule R M
inst✝¹ : Small.{u, u_3} ι
inst✝ : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2} ↥((DFinsupp.lsum ℕ) fun i ↦ (P i).subtype).range
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
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]

Goal state after:
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
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) y = (rTensor Q f).range.mkQ y
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (TensorProduct.comm R M N) x = (TensorProduct.comm R M N) (S.sum fun n m ↦ m ⊗ₜ[R] n)

Tactic:
h,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (S.sum fun m n ↦ m ⊗ₜ[R] n) = (TensorProduct.comm R M N) (S.sum fun n m ↦ m ⊗ₜ[R] n)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ x = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Tactic:
h,

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (S.sum fun m n ↦ m ⊗ₜ[R] n) = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2