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

Goal state before:
pp: case pos
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
have : 0 < b ^ k := by positivity
    simpa [h]

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

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
⊢ ∀ (tl : List Char), (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1

Tactic:
tl

Goal state after:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n : ℕ
c : Char
⊢ ∀ (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
tl

Goal state after:
case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n : ℕ
⊢ ofDigits (-1) [n] = (List.map (fun n ↦ ↑n) [n]).alternatingSum

Tactic:
by simp [ofDigits, List.alternatingSum]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ↑(Nat.find h✝)

pp: case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
next h_2 =>
        simp_all only [cast_le, le_find_iff, lt_find_iff, Decidable.not_not, le_refl,
          not_true_eq_false, not_false_eq_true, implies_true]

Goal state after:
case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
⊢ orderOf 1 = 1

Tactic:
by
  rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 ↦ x * x_1) 1 / (minimalPeriod (fun x_1 ↦ x * x_1) 1).gcd n

Tactic:
← minimalPeriod_iterate_eq_div_gcd' h,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 ↦ x ^ n * x_1) 1 = minimalPeriod (fun x_1 ↦ x * x_1)^[n] 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hb
p k : ℕ
hp : Prime p
⊢ 1 ≠ 0

pp: case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1

Tactic:
· exact one_ne_zero

Goal state after:
case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : i ≤ multiplicity m n
⊢ i < b

Tactic:
rw [← fin.pow_dvd_iff_le_multiplicity] at h

Goal state after:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : m ^ i ∣ n
⊢ i < b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b

Tactic:
rw [zero_pow, zero_dvd_iff] at h
              exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k) =
    x ^ p ^ n + y ^ p ^ n + ↑p * ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * ↑((p ^ n).choose k / p)

Tactic:
simp_rw [mul_sum]
    congr! 2 with k hk
    obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
    -- The maths is over now. We just commute things to their place.
    rw [Nat.cast_comm, mul_assoc (_ * _)]
    norm_cast
    rw [Nat.div_mul_cancel (hp.dvd_choose_pow _ _)] <;> lia

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ ((MulAction.toPermHom G α) y ^ k) a = a

Tactic:
MulAction.toPermHom_apply

Goal state after:
G : Type u_1
inst✝¹ : Group G
y : G
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ zpowers y
⊢ (MulAction.toPerm y ^ k) a = a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ ¬IsMulTorsionFree G ↔ ∃ a, a ≠ 1 ∧ IsOfFinOrder a

Tactic:
simp [isMulTorsionFree_iff_not_isOfFinOrder]

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

Goal state before:
pp: case pos
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
use b

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : n = 0
⊢ a = b ^ n ∧ b = b ^ m
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ M (C a * X ^ (n + 1))

Tactic:
rw [C_mul_X_pow_eq_monomial]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ M ((monomial (n + 1)) a)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (if p ∣ n * p then f.coeff (n * p / p) else 0) = f.coeff n

Tactic:
if_pos (dvd_mul_left _ _),

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ f.coeff (n * p / p) = f.coeff n
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + q * c • (p /ₘ q) = c • p

Tactic:
by rw [mul_smul_comm, ← smul_add, modByMonic_add_div]

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

Goal state before:
pp: S : Type v
R : Type u_1
inst✝³ : CommSemiring R
inst✝² : Nontrivial S
inst✝¹ : Semiring S
inst✝ : Algebra R S
p q : R[X]
h : IsCoprime p q
s : S
⊢ (aeval s) p ≠ 0 ∨ (aeval s) q ≠ 0

Tactic:
by
  by_contra! ⟨hp, hq⟩
  rcases h with ⟨_, _, h⟩
  apply_fun aeval s at h
  simp only [map_add, map_mul, map_one, hp, hq, mul_zero, add_zero, zero_ne_one] at h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (C (f.coeff 0))
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
isUnit_C

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit (C (f.coeff 0))

Tactic:
isUnit_C

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit (f.coeff 0)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n k : ℕ
f : R[X]
⊢ (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

Tactic:
induction k generalizing f <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
⊢ f₁ = f₂

Tactic:
have hle : f₁ ≤ f₂ := pi_le_pi.1 h.le

Goal state after:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
hle : f₁ ≤ f₂
⊢ f₁ = f₂
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
refine inf_le_of_right_le ?_

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine inf_le_of_right_le ?_

Goal state after:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4
α : 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.ker
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
le_cofinite_iff_ker.mp hq.1,

Goal state after:
case refine_4
α : 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 = (f.ker, Coheyting.boundary f)
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:
rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_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
⊢ (Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
k : ℕ
f : R[X]
⊢ (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

Tactic:
induction k generalizing f <;> simp [*]

Goal state after:
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 + 1)! * ∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
Nat.factorial_succ,

Goal state after:
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 + 1) * k !) * ∑ 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
⊢ ∀
    (ha :
      r ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match
        match r, ha with
        | (T, i), x => (T.erase i, i),
        ⋯ with
      | (T, i), x => (insert i T, i)) =
      r

Tactic:
hr

Goal state after:
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 |
      match x with
      | (T, i) => i ∈ T}
⊢ (match
      match r, hr with
      | (T, i), x => (T.erase i, i),
      ⋯ with
    | (T, i), x => (insert i T, i)) =
    r
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ p / GCDMonoid.gcd p q ≠ 0

Tactic:
hr

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
hr

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
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
⊢ ∀
    (ha :
      r ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match
        match r, ha with
        | (T, i), x => (insert i T, i),
        ⋯ with
      | (T, i), x => (T.erase i, i)) =
      r

Tactic:
hr

Goal state after:
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 |
      match x with
      | (T, i) => i ∉ T}
⊢ (match
      match r, hr with
      | (T, i), x => (insert i T, i),
      ⋯ with
    | (T, i), x => (T.erase i, i)) =
    r
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
n : ℕ
chn : ↑n ≠ 0
a : R[X]
⊢ derivative (a ^ n) = 0 ↔ derivative a = 0

Tactic:
by
  nontriviality R
  rw [← C_ne_zero, C_eq_natCast] at chn
  simp +contextual [derivative_pow, chn]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p = q

Tactic:
rw [← sub_eq_zero]
  apply eq_zero_of_infinite_isRoot
  simpa only [IsRoot, eval_sub, sub_eq_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
⊢ Disjoint (normalizedFactors a) (normalizedFactors b)

Tactic:
by
  rw [Multiset.disjoint_left]
  intro x hxa hxb
  have x_dvd_a := dvd_of_mem_normalizedFactors hxa
  have x_dvd_b := dvd_of_mem_normalizedFactors hxb
  exact (prime_of_normalized_factor x hxa).not_isUnit (hc x_dvd_a x_dvd_b)

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

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ False

Tactic:
exact
      (prime_of_normalized_factor _ hp).not_isUnit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
a x : R
⊢ x ∈ nthRootsFinset n a ↔ x ^ n = a

Tactic:
nthRootsFinset_def,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : 0 < n
a x : R
⊢ x ∈ (nthRoots n a).toFinset ↔ x ^ n = a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
k : ℕ
hi : (X ^ k).content = 1
⊢ (X ^ (k + 1)).content = 1

Tactic:
| succ k hi =>

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]
⊢ normUnit p.content = 1

Tactic:
by_cases hp0 : p.content = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : p.content = 0
⊢ normUnit p.content = 1

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ normUnit p.content = 1
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
by
  by_cases h : p = 0; · simp [h]
  rw [← content_eq_zero_iff] at h
  rw [isPrimitive_iff_content_eq_one, ← normalize_content, normalize_eq_one]
  refine isUnit_of_associated_mul (.symm ?_) h
  conv_lhs => rw [p.eq_C_content_mul_primPart]
  apply associated_content_C_mul

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

Tactic:
Nat.factorial_succ,

Goal state after:
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) * n !) ∈ nonZeroDivisors R
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (if hq : (q * C q.leadingCoeff⁻¹).Monic then (p.divModByMonicAux hq).2 else p) = p

Tactic:
dif_pos (monic_mul_leadingCoeff_inv hq0)

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (p.divModByMonicAux ⋯).2 = p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : (Associates.mk a).factors ⊓ (Associates.mk b).factors ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

Tactic:
factors_mk a ha,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a) ⊓ (Associates.mk b).factors ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
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
⊢ ↑(map (algebraMap R S) (s.prod f)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

Tactic:
Polynomial.map_prod,

Goal state after:
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
⊢ ↑(∏ i ∈ s, map (algebraMap R S) (f i)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 → ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

Tactic:
intro hg p ha hb hp
    refine (Associates.prime_mk.mpr hp).not_isUnit (isUnit_of_dvd_one ?_)
    rw [← hg]
    exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb)

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

Goal state before:
pp: case e_q
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹)) = q * C q.leadingCoeff⁻¹

Tactic:
rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = p * r

Tactic:
hr

Goal state after:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ p * r = p * r
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (gcd p q).degree ≤ q.degree

Tactic:
rw [gcd_comm]
  exact degree_gcd_le_left hq p

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
⊢ (algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥) = (↑(RingHom.id S)).comp (algebraMap R S)

Tactic:
ext; rfl

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
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ Function.Surjective ⇑g.rangeRestrict

Tactic:
← range_eq_top,

Goal state after:
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
this : g = g.range.subtype ∘ₗ g.rangeRestrict
⊢ g.rangeRestrict.range = ⊤
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
eq : (rTensor M (f ∘ₗ N'.subtype)) x = (rTensor M (f ∘ₗ N'.subtype)) y
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
eq :
  (rTensor M ((Submodule.map f N').subtype ∘ₗ f.submoduleMap N')) x =
    (rTensor M ((Submodule.map f N').subtype ∘ₗ f.submoduleMap N')) y
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y