mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
n : ℕ
h : p ≠ 0
⊢ rootMultiplicity a (p * (X - C a) ^ n) = rootMultiplicity a p + n

Tactic:
by
  have h2 := monic_X_sub_C a |>.pow n |>.mul_left_ne_zero h
  refine le_antisymm ?_ ?_
  · rw [rootMultiplicity_le_iff h2, add_assoc, add_comm n, ← add_assoc, pow_add,
      dvd_cancel_right_mem_nonZeroDivisors (monic_X_sub_C a |>.pow n |>.mem_nonZeroDivisors)]
    exact pow_rootMultiplicity_not_dvd h a
  · rw [le_rootMultiplicity_iff h2, pow_add]
    exact mul_dvd_mul_right (pow_rootMultiplicity_dvd p a) _

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
let : Invertible a := ha.invertible
  rcases eq_or_ne p 0 with rfl | hp; · simp
  rw [le_rootMultiplicity_iff hp]
  have h := pow_rootMultiplicity_dvd (p.comp (C a * X + C b)) c
  rw [dvd_comp_C_mul_X_add_C_iff, pow_comp] at h
  refine (pow_dvd_pow_of_dvd ((isUnit_C.mpr ha).dvd_mul_left.mp (dvd_of_eq ?_)) _).trans h
  simp [← map_mul, mul_sub, ← mul_assoc, sub_sub, add_comm, mul_add]

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

Goal state before:
pp: case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

pp: case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
· intros
      rw [Nat.cast_zero, mul_zero, zero_mul]

Goal state after:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (0, p).2.degree < q.degree

Tactic:
Classical.not_not.1 hp

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ (0, 0).2.degree < q.degree
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t

Tactic:
split_ifs with ha

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : a = x
⊢ count a (x ::ₘ t) = 1 + count a t

case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Tactic:
rw [smul_sum]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.coeff ((derivative p).natDegree + 1) * (↑(derivative p).natDegree + 1) = p.coeff p.natDegree * ↑p.natDegree

Tactic:
natDegree_derivative

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ p.coeff (p.natDegree - 1 + 1) * (↑(p.natDegree - 1) + 1) = p.coeff p.natDegree * ↑p.natDegree
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
⊢ pi f ⊓ 𝓟 (univ.pi s) = ⊥ ↔ ∃ i, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
by
  constructor
  · simp only [inf_principal_eq_bot, mem_pi]
    contrapose!
    rintro (hsf : ∀ i, ∃ᶠ x in f i, x ∈ s i) I - t htf hts
    have : ∀ i, (s i ∩ t i).Nonempty := fun i => ((hsf i).and_eventually (htf i)).exists
    choose x hxs hxt using this
    exact hts (fun i _ => hxt i) (mem_univ_pi.2 hxs)
  · simp only [inf_principal_eq_bot]
    rintro ⟨i, hi⟩
    filter_upwards [mem_pi_of_mem i hi] with x using mt fun h => h i trivial

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : t₁ ×ˢ t₂ ⊆ s
⊢ s ∈ f ×ˢ g
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f

Tactic:
by
  rw [← principal_univ, mem_prod_principal]
  simp only [mem_univ, forall_true_left]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
exact
    sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left)
      (inf_le_inf_left _ <| hnot_anti le_sup_right)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set (α × β)
⊢ sᶜ ∈ cofinite.coprod cofinite ↔ sᶜ ∈ cofinite

Tactic:
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ ↑(n.descFactorial n) = ↑n !

Tactic:
n.descFactorial_self

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ ↑n ! = ↑n !
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (-p).roots = p.roots

Tactic:
← neg_one_smul R p,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (-1 • p).roots = p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit p

Tactic:
apply (hs p (Multiset.mem_cons_self _ _)).2.1

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ Prime p ∧ p ∣ x → p ∈ normalizedFactors x

Tactic:
· rintro ⟨hprime, hdvd⟩
    obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd
    rw [associated_iff_eq] at hqeq
    exact hqeq ▸ hqmem

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ ↑(Classical.choose ⋯).card < ↑(Classical.choose ⋯).card

Tactic:
Nat.cast_lt

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ (Classical.choose ⋯).card < (Classical.choose ⋯).card
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map (algebraMap T S) p).aroots R = p.aroots R

Tactic:
by
  rw [aroots_def, aroots_def, map_map, IsScalarTower.algebraMap_eq T S R]

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

Goal state before:
pp: T : Type w
inst✝⁸ : CommRing T
p : T[X]
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') p = 0
⊢ map (algebraMap T S) p = 0

Tactic:
obtain rfl : p = 0 :=
    map_injective _ (FaithfulSMul.algebraMap_injective T S') (by rwa [Polynomial.map_zero])

Goal state after:
T : Type w
inst✝⁸ : CommRing T
inst✝⁷ : IsDomain T
S : Type u_1
S' : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra T S
inst✝³ : CommRing S'
inst✝² : IsDomain S'
inst✝¹ : Algebra T S'
inst✝ : Module.IsTorsionFree T S'
f : S →ₐ[T] S'
h₀ : map (algebraMap T S') 0 = 0
⊢ map (algebraMap T S) 0 = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ (p₁ + p₂) % q = p₁ % q + p₂ % q

Tactic:
by
  simp [Polynomial.mod_def, Polynomial.add_modByMonic]

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
⊢ a ∣ Quot.out (Associates.mk c ⊓ Associates.mk b)

Tactic:
by
    rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le, le_inf_iff,
      mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]
    exact ⟨hac, hab⟩

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, leadingCoeff 0)

Tactic:
Polynomial.leadingCoeff_zero

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, 0)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ ↑a.natDegree < ↑(a.natDegree + c.natDegree)

Tactic:
Nat.cast_lt

Goal state after:
case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ a.natDegree < a.natDegree + c.natDegree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (C x)

Tactic:
· exact fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
⊢ False

Tactic:
cases mul_eq_zero.mp h

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : a = 0
⊢ False

case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h✝ : b = 0
⊢ False
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑g.symm ∘ₗ ↑f = (↑g.symm ∘ₗ ↑f) ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
comp_coe,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑(f ≪≫ₗ g.symm) = ↑(f ≪≫ₗ g.symm) ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case convert_2
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) = (algebraMap K L) 0

Tactic:
RingHom.map_zero

Goal state after:
case convert_2
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
Module: Mathlib.Algebra.Colimit.TensorProduct

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) x)) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M ↑(Module.fgSystem.equiv R P).symm) ((LinearMap.rTensor M (↑N).subtype) y))
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
← LinearMap.rTensor_comp_apply,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : { x // x.FG }
x y : ↥↑N ⊗[R] M
eq :
  (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (↑(Module.fgSystem.equiv R P).symm ∘ₗ (↑N).subtype)) x) =
    (directLimitLeft (Module.fgSystem R P) M)
      ((LinearMap.rTensor M (↑(Module.fgSystem.equiv R P).symm ∘ₗ (↑N).subtype)) y)
⊢ ∃ N', N'.FG ∧ ∃ (h : ↑N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
inst✝⁸ : (i : ι) → AddCommMonoid (G i)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑(e i) ∘ₗ ↑(e i).symm

Tactic:
comp_coe,

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
inst✝⁸ : (i : ι) → AddCommMonoid (G i)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑((e i).symm ≪≫ₗ e i)
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 ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑(e i) ∘ₗ ↑(e i).symm

Tactic:
comp_coe,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ f' i j h = f' i j h ∘ₗ ↑((e i).symm ≪≫ₗ e i)
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
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ q ⊗ₜ[R] h (r • p) - r • q ⊗ₜ[R] h p ∈ (lTensor Q f).range

Tactic:
← TensorProduct.tmul_smul,

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
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ q ⊗ₜ[R] h (r • p) - q ⊗ₜ[R] (r • h p) ∈ (lTensor Q f).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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ n ⊗ₜ[R] (h (g q) - q) ∈ (lTensor Q f).range

Tactic:
apply le_comap_range_lTensor f n

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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ h (g q) - q ∈ f.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
hg : Surjective ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh) (((lTensor Q f).range.liftQ (lTensor Q g) ⋯) ((lTensor Q f).range.mkQ y)) =
    (lTensor Q f).range.mkQ y

Tactic:
simp only [Submodule.mkQ_apply, Submodule.liftQ_apply, lTensor.inverse_of_rightInverse_apply]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
⊢ nilpotencyClass x = 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Goal state after:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
⊢ IsNilpotent x

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Goal state after:
R : Type u_1
x : R
inst✝¹ : Zero R
inst✝ : Pow R ℕ
hx : 0 < nilpotencyClass x
s : Set ℕ := {k | x ^ k = 0}
⊢ IsNilpotent x
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Goal state after:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Module.End R (Matrix n n R)
i j k l : n
⊢ (∑ x,
        f (single x.1.2 x.2.1 1) x.1.1 x.2.2 •
          ((mulLeftRight R (Matrix n n R)).toLinearMap (single x.1.1 x.1.2 1 ⊗ₜ[R] op (single x.2.1 x.2.2 1)))
            (single i j 1))
      k l =
    f (single i j 1) k l

Tactic:
simp [sum_apply, Matrix.mul_apply, single, Fintype.sum_prod_type, ite_and]

Goal state after: