mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ ((⇑derivative)^[k + 1] p).coeff m = (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1)

Tactic:
Function.iterate_succ_apply',

Goal state after:
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 : ℕ
⊢ (derivative ((⇑derivative)^[k] p)).coeff m = (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑m + 1)
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsAlgebraic R A
⊢ Nontrivial R

Tactic:
by
  obtain ⟨p, hp, -⟩ := Algebra.IsAlgebraic.isAlgebraic (R := R) (0 : A)
  exact .of_polynomial_ne hp

Goal state after:
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.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    ((m.succ + k - k) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ)

Tactic:
add_tsub_cancel_right

Goal state after:
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.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    (m.succ * (m.succ + k).descFactorial k) • p.coeff (m + k.succ)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ (⇑derivative)^[n + 1] (p * q) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))

Tactic:
Function.iterate_succ_apply',

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative ((⇑derivative)^[n] (p * q)) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
congr 1

Goal state after:
case inr.refine_1.e_a
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q) + 0

Tactic:
add_zero

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Tactic:
untopD_coe_enat

Goal state after:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x

Tactic:
rootMultiplicity_eq_zero_iff,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ ¬(p.IsRoot x → p = 0) ↔ p ≠ 0 ∧ p.IsRoot x
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ (⇑derivative)^[k + 1] (X ^ n) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
Function.iterate_succ_apply',

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ derivative ((⇑derivative)^[k] (X ^ n)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      I.Finite ∧
        ∃ V, (∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i) ∧ (∀ i ∉ I, V i = univ) ∧ s = ⋂ i ∈ I, V i ∧ s = ⋂ i, V i) →
    ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I, eval a ⁻¹' t a ⊆ s

Tactic:
rintro ⟨I, If, V, hVf, -, rfl, -⟩

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = C ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
iterate_derivative_X_pow_eq_natCast_mul n k,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ ↑(n.descFactorial k) * X ^ (n - k) = C ↑(n.descFactorial k) * X ^ (n - k)
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
⊢ ¬(X - 0) ^ (p.natTrailingDegree + 1) ∣ p

Tactic:
sub_zero,

Goal state after:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ¬X ^ (p.natTrailingDegree + 1) ∣ p
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
⊢ (X - 0) ^ p.natTrailingDegree ∣ p

Tactic:
sub_zero,

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ X ^ p.natTrailingDegree ∣ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
by
  by_cases h : p = 0
  · simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]
  refine le_antisymm ?_ ?_
  · rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]
    exact ⟨p.natTrailingDegree,
      fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt_add_one _⟩
  · rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]
    exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ 1 + 0 = 1

Tactic:
add_zero

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
hgu : IsUnit g
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.succ
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)

Tactic:
exact Nat.div_mul_cancel (Nat.two_dvd_mul_add_one _)

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

Goal state before:
pp: case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ ￢f

pp: case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary f ≤ q.2

Tactic:
· rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]
      exact hq.2.1

Goal state after:
case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary f ≤ q.2
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ↑k ! * ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑k ! * (↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a))

Tactic:
congr 1

Goal state after:
case e_a
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ b ∈ powersetCard (#S - k) S, derivative (∏ a ∈ b, (X - C a)) =
    ↑(k + 1) * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
⊢ (insert r.2 (r.1.erase r.2), r.2) = r

Tactic:
congr 1

Goal state after:
case left_neg.e_fst
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
⊢ insert r.2 (r.1.erase r.2) = r.1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
⊢ ((insert r.2 r.1).erase r.2, r.2) = r

Tactic:
congr 1

Goal state after:
case right_neg.e_fst
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
⊢ (insert r.2 r.1).erase r.2 = r.1
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
⊢ Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots = p.roots

Tactic:
set f := fun x ↦ a * x + b
  have hf : Function.Bijective f :=
    (AddGroup.addRight_bijective b).comp (IsUnit.isUnit_iff_mulLeft_bijective.mp ha)
  rw [Multiset.ext]
  intro x
  obtain ⟨x, rfl⟩ := hf.surjective x
  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.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
S : Finset R
hS : ∀ x ∈ S, eval x p = 0
hcard : p.degree ≤ ↑(#S)
hp : p ≠ 0
⊢ p.roots = S.val

Tactic:
by
  refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm
  · exact (Finset.val_le_iff_val_subset.mpr (fun x hx ↦ (p.mem_roots hp).mpr (hS x hx)))
  · simpa using (p.card_roots hp).trans hcard

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n - 0).roots = replicate n 0

Tactic:
sub_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
⊢ (X ^ n).roots = replicate n 0
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
⊢ Associates.mkMonoidHom (map (Classical.choose ⋯) (normalizedFactors x)).prod = x

Tactic:
MonoidHom.map_multiset_prod,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
⊢ content 1 = 1

Tactic:
rw [← C_1, content_C, normalize_one]

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

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

Tactic:
rw [Nat.cast_zero, Nat.WithBot.lt_zero_iff, degree_eq_bot, mul_eq_zero] at hpq
      rcases hpq with (rfl | rfl) <;> simp

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

Goal state before:
pp: 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✝

Tactic:
congr 1

Goal state after:
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: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α f = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α g = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

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

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

Tactic:
add_zero

Goal state after:
case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count a.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : 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
hb0 : p.count b.factors = 0
⊢ p.count a.factors + 0 = p.count a.factors

Tactic:
add_zero

Goal state after:
case neg.inr
α : 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
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count a.factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : x = 0
⊢ False

Tactic:
← hf,

Goal state after:
case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible (C x)
hf : C x = f
hx : x = 0
⊢ False
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)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k

Tactic:
obtain ⟨u, hu⟩ := Multiset.exists_smul_of_dvd_count _ hk'

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)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ ∃ b, Associates.mk a0 = b ^ k
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
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
⊢ Function.Injective ⇑(algebraMap R A)

Tactic:
by convert! inj.comp C_injective; ext; simp

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

Goal state before:
pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (p : K[X]), p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
intro p hp ih _ne_zero aeval_eq
    rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq
    rcases aeval_eq with aeval_eq | x_eq
    · exact ih hp aeval_eq
    · rw [x_eq, Subalgebra.coe_zero, inv_zero]
      exact A.zero_mem

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

Goal state before:
pp: case add
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
x y : Q ⊗[R] P
hx : ∃ a, (lTensor Q g) a = x
hy : ∃ a, (lTensor Q g) a = y
⊢ ∃ a, (lTensor Q g) a = x + y

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
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
x y : P ⊗[R] Q
hx : ∃ a, (rTensor Q g) a = x
hy : ∃ a, (rTensor Q g) a = y
⊢ ∃ a, (rTensor Q g) a = x + y

Tactic:
| add x y hx hy =>

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'
⊢ (lTensor P g').ker = (lTensor P f').range

Tactic:
Exact.linearMap_ker_eq (lTensor_exact P hfg' hg')

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
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'
⊢ (lTensor P f').range = (lTensor P f').range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case add
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 y : M ⊗[R] N
hx : ∃ S, x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum
hy : ∃ S, y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum
⊢ ∃ S, x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case add
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 y : M ⊗[R] N
hx : ∃ S, x = S.sum fun m n ↦ m ⊗ₜ[R] n
hy : ∃ S, y = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case a.refine_4.tmul.add
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
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case a.add
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 y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
hy :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y) ∈
    ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
| add x y hx hy =>

Goal state after: