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
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
⊢ a ^ n ∈ H

Tactic:
rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
⊢ a ^ n ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod (n + 1)
⊢ a * a⁻¹ = ↑(a.val.gcd (n + 1))

Tactic:
· calc
      a * a⁻¹ = a * a⁻¹ + n.succ * Nat.gcdB (val a) n.succ := by
        rw [natCast_self, zero_mul, add_zero]
      _ = ↑(↑a.val * Nat.gcdA (val a) n.succ + n.succ * Nat.gcdB (val a) n.succ) := by
        push_cast
        rw [natCast_zmod_val]
        rfl
      _ = Nat.gcd a.val n.succ := by rw [← Nat.gcd_eq_gcd_ab a.val n.succ]; rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ n.properDivisors, x = 1 ↔ Prime n

Tactic:
by
  rcases n with - | n
  · simp [Nat.not_prime_zero]
  · cases n
    · simp [Nat.not_prime_one]
    · rw [← properDivisors_eq_singleton_one_iff_prime]
      refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
      rw [@eq_comm (Finset ℕ) _ _]
      apply
        eq_properDivisors_of_subset_of_sum_eq_sum
          (singleton_subset_iff.2
            (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
          ((sum_singleton _ _).trans h.symm)

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
· rw [if_pos h, h, val_zero, tsub_zero, Nat.mod_self]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ m * a).val = a.val ^ (m + 1)

Tactic:
ZMod.val_mul,

Goal state after:
case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ m).val * a.val % n = a.val ^ (m + 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b [0] = ofDigits b l

Tactic:
ofDigits_singleton,

Goal state after:
b : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * 0 = ofDigits b l
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]

Goal state after:
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≤ 1
n : ℕ
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
by
  simp [maxPowDvdDiv, Nat.not_lt_of_ge hp]

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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) l1 l2)

Tactic:
induction l1 generalizing l2 with

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
⊢ ¬x ^ n = 1

Tactic:
hnx

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Tactic:
cases hm : min (emultiplicity p a) (emultiplicity p b)
  · simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢
    contrapose hm
    simp only [not_and_or, not_not] at hm ⊢
    exact hm.or_of_add
  · apply le_emultiplicity_of_pow_dvd
    simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (fixedLengthDigits hb l).card = b ^ l

Tactic:
Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l),

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ (Finset.range (b ^ l)).card = b ^ l
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
by
  if hn : n = 0 then simp [hn] else
  if pp : p.Prime then ?_ else
    simp [pp]
  ext q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp
  · rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]

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

Goal state before:
pp: a b c : ℕ
h : b ∣ c
hb : b ≠ 0
hc : c ≠ 0
⊢ b.factorization a ≤ c.factorization a

Tactic:
obtain ⟨k, rfl⟩ := h; simp [factorization_mul hb (Nat.ne_zero_of_mul_ne_zero_right hc)]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
← mul_one (x ^ m),

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m * 1 ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
· let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
    simp [hr]

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k : ℕ
hp : Prime p
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => dvd_choose_pow hp h.1 h.2⟩

Goal state after:
case refine_1
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ 0

case refine_2
p n k : ℕ
hp : Prime p
h : p ∣ (p ^ n).choose k
⊢ k ≠ p ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ g ^ H.index ∈ H

Tactic:
← eq_one_iff,

Goal state after:
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ ↑(g ^ H.index) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ m * a.factorization p = n * b.factorization p

Tactic:
simpa using congr(factorization $h p)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ CharP R (p ^ n)

Tactic:
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]

Goal state after:
R : Type u_6
inst✝¹ : Ring R
inst✝ : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
⊢ CharP R (p ^ n)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
n : ℕ
this : rootMultiplicity a (C 1 * (X - C a) ^ n) = rootMultiplicity a (C 1) + n
⊢ rootMultiplicity a ((X - C a) ^ n) = n

Tactic:
rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
h✝ : IsUnit p
u : R
h : C u = p
⊢ 1 ≤ 0

Tactic:
simp [← hp, ← h, degree_C_le]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ natDegree 0 < p.natDegree

Tactic:
Polynomial.natDegree_zero

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ 0 < p.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ∀ b ∈ p.support, ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) b (p.coeff b)).degree ≤ ↑(p.natDegree - 1)

Tactic:
intro n hn

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
n : ℕ
hn : n ∈ p.support
⊢ ((fun n a ↦ C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.natDegree - 1 ∈ (derivative p).support

Tactic:
rw [mem_support_derivative, tsub_add_cancel_of_le (by lia), mem_support_iff,
      coeff_natDegree, leadingCoeff_ne_zero]

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (g.comp (X + C t)).coeff (g.comp (X + C t)).natTrailingDegree

Tactic:
Nat.le_zero.1 (natTrailingDegree_le_of_ne_zero <|
      this ▸ eval_divByMonic_pow_rootMultiplicity_ne_zero t hp),

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (g.comp (X + C t)).coeff 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (n ≤ if h0 : p = 0 then 0 else Nat.find ⋯) ↔ (X - C a) ^ n ∣ p

Tactic:
dif_neg p0,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ Nat.find ⋯ ↔ (X - C a) ^ n ∣ p
Module: Mathlib.Order.Filter.Prod

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

Tactic:
by
  rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
  refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
  · rintro ⟨v, v_in, hv⟩ a a_in b b_in
    exact hv (mk_mem_prod a_in <| v_in b_in)
  · rintro ⟨x, y⟩ ⟨hx, hy⟩
    exact h hx y hy

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ∂ ⊤ = ⊥

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
⊢ ⊤ ⊓ ￢⊤ = ⊥
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊓ ￢￢￢a = ￢a ⊓ ￢￢a
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢(a ⊓ ￢a) = ⊤
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
inf_sup_left,

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

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

Tactic:
boundary,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
⊢ comap Prod.fst f ⊓ comap Prod.snd ⊤ = comap Prod.fst f

Tactic:
comap_top,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
⊢ comap Prod.fst f ⊓ ⊤ = comap Prod.fst f
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ comap Prod.fst ⊤ ⊓ comap Prod.snd g = comap Prod.snd g

Tactic:
comap_top,

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
⊢ ⊤ ⊓ comap Prod.snd g = comap Prod.snd g
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ ∂ a = ∂ a

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ a ⊓ ￢∂ a = ∂ a
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ ∂ a = a

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ a ⊓ ￢a = a
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
boundary,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ a ⊓ ￢a = a
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' (s + t) = ⇑ofAdd '' s * ⇑ofAdd '' t

Tactic:
by
  rw [← Set.image2_add, Set.image_image2_distrib ofAdd_add, Set.image2_mul]

Goal state after:
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).ker ∪ q.2.ker
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
ker_principal,

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.2.ker
⊢ q = (f.ker, Coheyting.boundary f)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
h : p ∣ s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q

Tactic:
· rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
      exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p ↦ p) s.val, a ∣ n

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using div

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case pos
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∈ f.support
⊢ 0 < w s

Tactic:
exact Nat.zero_lt_of_ne_zero hs

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
⊢ normalizedFactors 0 = 0

Tactic:
by
  simp [normalizedFactors, factors]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ normalizedFactors 1 = 0

pp: case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0

Tactic:
· dsimp [normalizedFactors, factors]
    simp [Subsingleton.elim (1 : α) 0]

Goal state after:
case inr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ normalizedFactors 1 = 0
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
by rw [H, C_0, roots_zero]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (fun x ↦ x) (normalizedFactors (x * y)) =
    Multiset.map (fun x ↦ x) (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)

Tactic:
← Multiset.map_congr rfl normalize_normalized_factor,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map normalize (normalizedFactors (x * y)) =
    Multiset.map (fun x ↦ x) (normalizedFactors x) + Multiset.map (fun x ↦ x) (normalizedFactors y)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ ∀ x ∈ p.support, p.coeff x = 0

Tactic:
· intro x
    simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd p.coeff) =
    gcd a ((Finset.range (max p.natDegree q.natDegree).succ).gcd q.coeff)

Tactic:
apply Finset.gcd_eq_of_dvd_sub

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ ∀ x ∈ Finset.range (max p.natDegree q.natDegree).succ, a ∣ p.coeff x - q.coeff x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case hα
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0

Tactic:
simp only [associated_zero_iff_eq_zero] at this

Goal state after:
case hα
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
this : a = 0 ↔ b = 0
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ (Associates.mk a).factors.prod = Associates.mk a

Tactic:
simp [ha, prod_mk, mk_eq_mk_iff_associated, UniqueFactorizationMonoid.factors_prod]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
le_rootMultiplicity_iff hmap,

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
b : B
⊢ (X - C b) ^ count b (Multiset.map (⇑f) p.roots) ∣ map f p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_2
α : 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 ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ a

pp: case refine_3
α : 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 ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ b

Tactic:
· apply dvd_of_mk_le_mk
    apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left
    apply ha

Goal state after:
case refine_3
α : 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 ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
by_cases H : x = 0
  · rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
  · classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ ¬map (algebraMap R S) p = 0

Tactic:
← degree_eq_bot,

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ ¬(map (algebraMap R S) p).degree = ⊥
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
  have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))
  rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key
  exact ⟨q.coeff 0, hq0, key⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.Small

Goal state before:
pp: ι : Type u
π : ι → Type v
inst✝² : (i : ι) → Zero (π i)
inst✝¹ : Small.{w, u} ι
inst✝ : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq : (fun x j ↦ x j) f = (fun x j ↦ x j) f'
⊢ f = f'

Tactic:
by ext j; exact congr_fun eq j

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
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
p p' : P
q : Q
⊢ ((TensorProduct.mk R N Q) (h (p + p'))) q -
      (fun x1 x2 ↦ x1 + x2) (((TensorProduct.mk R N Q) (h p)) q) (((TensorProduct.mk R N Q) (h p')) q) ∈
    (rTensor Q f).range

Tactic:
by
      change h (p + p') ⊗ₜ[R] q - (h p ⊗ₜ[R] q + h p' ⊗ₜ[R] q) ∈ range (rTensor Q f)
      rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]
      apply le_comap_range_rTensor f
      rw [exact_iff] at hfg
      simp only [← hfg, mem_ker, map_sub, map_add, hgh _, sub_self]

Goal state after: