mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
⊢ False

Tactic:
let f : (Set.Icc 0 H.index) → G ⧸ H := fun n ↦ (a ^ (n : ℕ) : G)

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
⊢ False
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n.succ | d ∣ n} = n.divisors

Tactic:
ext
  simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors.Nonempty ↔ 1 < n

Tactic:
exact nonempty_properDivisors

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal ↔ x✝ ∈ ↑n.divisorsAntidiagonal

Tactic:
exact swap_mem_divisorsAntidiagonal

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors ⊆ s

Tactic:
← sdiff_eq_empty_iff_subset

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors \ s = ∅
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
by_cases lt : n + 1 < k
  · simp [choose_eq_zero_of_lt lt]
  · cases n with
    | zero => cases k <;> simp_all
    | succ n =>
      rcases k with - | k
      · rw [choose_zero_right]
        exact Nat.one_le_two_pow
      · rw [choose_succ_succ', two_pow_succ]
        exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
obtain ⟨m, he⟩ := he

Goal state after:
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ x.natAbs ≤ y.natAbs
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Goal state after:
case inl.inl
n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ 0 ∣ n ↔ 0 ≤ padicValNat 0 n

case inl.inr
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
hk : k > 0
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
⊢ D :: L = L2

Tactic:
obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm

Goal state after:
case cons
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
len : (D :: L).length = (d :: l).length
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : ofDigits b (D :: L) = ofDigits b (d :: l)
⊢ D :: L = d :: l
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b ≤ ↑n
⊢ multiplicity a b ≤ n

Tactic:
exact_mod_cast multiplicity_le_emultiplicity.trans h

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

Goal state before:
pp: case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)

Tactic:
exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
· rw [dvd_add_right]
    · apply this.not_pow_dvd_of_multiplicity_lt
      simp
    apply pow_dvd_of_le_emultiplicity
    exact Order.add_one_le_of_lt h

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
exact multiplicity_mul hp hfin

Goal state after:
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
⊢ (∏ x ∈ Ico 1 (p * (n + 1) + 1), x).factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left),

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
⊢ ∑ x ∈ Ico 1 (p * (n + 1) + 1), x.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1
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 * (n + 1)).factorization p) =
    (∏ x ∈ Ico 1 (p * n + 1), x).factorization p + ((n + 1).factorization p + 1)

Tactic:
factorization_prod_apply (fun _ hx ↦ ne_zero_of_lt
    (mem_Ico.mp hx).left),

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 + (p * (n + 1)).factorization p) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ (n + 1).factorization p ≤ ((n + 1).choose (k + 1) * (k + 1)).factorization p

Tactic:
refine factorization_le_factorization_of_dvd_right ?_ (zero_ne_add_one n).symm
      (Nat.mul_ne_zero (ne_of_gt <| choose_pos hkn) (by positivity))

Goal state after:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
| succ N ih =>

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
simp only [hp0, zero_divByMonic, le_refl]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R p) f) = p * rootMultiplicity (r ^ p) f

Tactic:
← pow_one p,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
⊢ rootMultiplicity r ((expand R (p ^ 1)) f) = p ^ 1 * rootMultiplicity (r ^ p ^ 1) f
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) * q +
        -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree <
    q.natDegree

Tactic:
tsub_eq_zero_iff_le.mpr h,

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * X ^ 0 * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
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 + k).succ.descFactorial k • p.coeff (m + k.succ) * ↑(m + 1) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)

Tactic:
← nsmul_eq_mul',

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∑ i, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Tactic:
exact
    (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
      (sum_monomial_eq _)

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ ¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0

Tactic:
← nsmul_eq_mul',

Goal state after:
R : Type u
n : ℕ
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
⊢ ¬(n + 1) • p.coeff (n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : 0 = p.coeff (m + 1) * ↑(m + 1)
⊢ False

Tactic:
← nsmul_eq_mul',

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : ∀ (n : ℕ), (derivative p).coeff n = coeff 0 n
hp' : p ≠ 0
f_nat_degree_pos : 0 < p.natDegree
m : ℕ := p.natDegree - 1
hm : m + 1 = p.natDegree
h2 : 0 = (m + 1) • p.coeff (m + 1)
⊢ False
Module: Mathlib.Order.Filter.Finite

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

Tactic:
induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ derivative (p ^ 2) = C 2 * p * derivative p

Tactic:
derivative_pow_succ,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ C (↑1 + 1) * p ^ 1 * derivative p = C 2 * p * derivative p
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
I' : Set ι
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I'.pi t ⊆ I.pi s
x : α i
hx : x ∈ t i
g : (i : ι) → α i
hg : ∀ (i : ι), g i ∈ t i
j : ι
x✝ : j ∈ I'
⊢ update g i x j ∈ t j

Tactic:
rcases eq_or_ne j i with (rfl | hne) <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b

Tactic:
unfold boundary
  rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ (map Prod.mk f).seq (pure b) = map (fun a ↦ (a, b)) f

Tactic:
seq_pure,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
b : β
⊢ map (fun g ↦ g b) (map Prod.mk f) = map (fun a ↦ (a, b)) f
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
hx₀ : x ≠ 0
⊢ normalizedFactors x = 0

Tactic:
normalizedFactors_eq_zero_iff hx₀

Goal state after:
case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
hx₀ : x ≠ 0
⊢ IsUnit x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
H : IsUnit q
hr : r ≠ 0
⊢ False

Tactic:
obtain ⟨s, hs, rfl⟩ := Polynomial.isUnit_iff.mp H

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
hr : r ≠ 0
s : R
hs : IsUnit s
hq : p = C r * C s
H : IsUnit (C s)
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (C a * p).aroots S = p.aroots S

Tactic:
aroots_C_mul _ ha

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ p.aroots S = p.aroots S
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 = p.natDegree

pp: case right.inr.right
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
⊢ q.roots = 0

Tactic:
· conv_rhs => rw [he]
    rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]

Goal state after:
case right.inr.right
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
⊢ q.roots = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
⊢ False

Tactic:
← factorSetMem_eq_mem,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : FactorSetMem s p
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
⊢ p.roots.card ≤ 1

Tactic:
by
  obtain hp | ⟨x, hx⟩ := p.roots.empty_or_exists_mem
  · simp [hp]
  convert! p.card_roots'
  exact (natDegree_eq_of_degree_eq_some <| degree_eq_one_of_irreducible_of_root hirr <|
    isRoot_of_mem_roots hx).symm

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
⊢ p.roots = 0

Tactic:
by_contra hroots

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
hdeg : p.natDegree ≠ 1
hroots : ¬p.roots = 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors.prod.factors = (a.factors + b.factors).prod.factors

Tactic:
prod_add,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors.prod.factors = (a.factors.prod * b.factors.prod).factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (map f (EuclideanDomain.gcd p q)) ↔ IsUnit (EuclideanDomain.gcd p q)

Tactic:
isUnit_map

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (EuclideanDomain.gcd p q) ↔ IsUnit (EuclideanDomain.gcd p q)
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
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ((monomial n) a).rootSet S = {0}

Tactic:
rootSet_monomial hn ha

Goal state after:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ {0} = {0}
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑(u⁻¹ * u) = 1

Tactic:
inv_mul_cancel

Goal state after:
case pos
R : Type u
inst✝ : Field R
u : R[X]ˣ
n : ℕ
h✝ : n = 0
⊢ eval 0 ↑1 = 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]

Goal state after:
case neg
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : ¬a = 0
⊢ C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (C a * (q * (C a⁻¹ * C q.leadingCoeff⁻¹))))) =
    C a⁻¹ * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)))
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)
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 = 0

Tactic:
eq_zero_of_ne q hq h

Goal state after:
case neg
α : 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
⊢ 0 = 0
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
x : k
⊢ ∃ y, (algebraMap K D) y = (algebraMap k D) x

Tactic:
exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsTorsionFree K L
inst✝ : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
⊢ Function.Bijective ⇑f

Tactic:
refine ⟨f.injective, fun b ↦ ?_⟩
  obtain ⟨p, hp, he⟩ := Algebra.IsAlgebraic.isAlgebraic (R := K) b
  let f' : p.rootSet L → p.rootSet L := (rootSet_maps_to' (fun x ↦ x) f).restrict f _ _
  have : f'.Surjective := Finite.injective_iff_surjective.1
    fun _ _ h ↦ Subtype.ext <| f.injective <| Subtype.ext_iff.1 h
  obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩
  exact ⟨a, Subtype.ext_iff.1 ha⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
t : S
ht : t ∈ R[s]
a✝ : ⟨t, ht⟩ ∈ ⊤
⊢ ⟨t, ht⟩ ∈ (aeval ⟨s, ⋯⟩).range

Tactic:
obtain ⟨r, rfl⟩ := adjoin_mem_exists_aeval _ _ ht

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ ⟨(aeval s) r, ht⟩ ∈ (aeval ⟨s, ⋯⟩).range
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
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)) = ((algebraMap K L) (-p.coeff 0))⁻¹ * ↑((aeval x) p.divX)

Tactic:
map_neg,

Goal state after:
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]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
this : (aeval ↑x) p = 0
⊢ -(((algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)) = (-(algebraMap K L) (p.coeff 0))⁻¹ * ↑((aeval x) p.divX)
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
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : (aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
revert ne_zero aeval_eq

Goal state after:
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 ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : DirectLimit.lift f ih compat ⟦⟨i, x⟩⟧ = DirectLimit.lift f ih compat ⟦⟨i, y⟩⟧
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧

Tactic:
by simp_rw [lift_def] at eq; rw [h i eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) x) =
    (LinearMap.rTensor M (of R ι G f x✝²)) x

Tactic:
by refine x.induction_on ?_ ?_ ?_ <;> aesop

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 ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f j k hjk) y) = w

Tactic:
rw [of_f, hy]

Goal state after: