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

Goal state before:
pp: case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0

Tactic:
left

Goal state after:
case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n ≤ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp
  · exact Nat.le_of_lt <| padicValNat_lt_self hn

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

Goal state before:
pp: case cons
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
l2 : List ℕ
h : (hd₁ :: tl₁).length = l2.length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) l2)

Tactic:
induction l2 generalizing tl₁ with

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

Goal state before:
pp: b m : ℕ
⊢ m < (b + 2) ^ ((b + 2).digits m).length

Tactic:
by
  convert! @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
  rw [ofDigits_digits (b + 2) m]

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

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

Tactic:
by
  induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial

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

Goal state before:
pp: n i b : ℕ
⊢ ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)

Tactic:
rw [List.getD_eq_getElem?_getD]

Goal state after:
n i b : ℕ
⊢ ((b + 2).digits n)[i]?.getD 0 = n / (b + 2) ^ i % (b + 2)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
have : FiniteMultiplicity p b := finiteMultiplicity_iff_emultiplicity_ne_top.2 (by simp [·] at h)
  rw [this.emultiplicity_eq_multiplicity] at *
  apply emultiplicity_eq_of_dvd_of_not_dvd
  · apply dvd_add
    · apply pow_dvd_of_le_emultiplicity
      exact h.le
    · simp
  · 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 inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
· contradiction

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
· contradiction

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / n)) = n

Tactic:
rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]
  rw [← Nat.div_mul_cancel hn] at hx; exact left_ne_zero_of_mul hx

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

Goal state before:
pp: m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ p ^ k * m / p ^ (p ^ k * m).factorization p = m

Tactic:
rw [ordCompl_self_pow_mul m k hp]
  exact (ordCompl_eq_self_iff_zero_or_not_dvd m hp).mpr (Or.inr hm)

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

Goal state before:
pp: p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k + (n - k) < succ 2 * p

Tactic:
add_tsub_cancel_of_le hkn

Goal state after:
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ n < succ 2 * p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
hn : n < p ^ i
⊢ k + (n - k) < p ^ i

Tactic:
add_tsub_cancel_of_le hkn

Goal state after:
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
hn : n < p ^ i
⊢ n < p ^ i
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n ! / (k ! * (n - k)!)).factorization p = 0

Tactic:
factorization_div (factorial_mul_factorial_dvd_factorial hnk),

Goal state after:
case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n !.factorization - (k ! * (n - k)!).factorization) p = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ (b / p ^ b.factorization p).factorization

Tactic:
factorization_ordCompl b p

Goal state after:
case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
⊢ Finsupp.erase p a.factorization ≤ Finsupp.erase p b.factorization
Module: Mathlib.Algebra.CharP.Lemmas

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

Tactic:
rw [Nat.div_mul_cancel (hp.dvd_choose_pow _ _)]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ p ^ n
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mp
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
· rintro ⟨x, rfl⟩
    rw [of'_mul_modOf]

Goal state after:
case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b m n : ℕ
hmn : m ≠ 0 ∨ n ≠ 0
h : a ^ m = b ^ n
⊢ ∃ c, a = c ^ (n / m.gcd n) ∧ b = c ^ (m / m.gcd n)

Tactic:
set g := gcd m n
  let m' := m / gcd m n
  let n' := n / gcd m n
  have coprime : m'.Coprime n' := by
    rcases hmn with hm | hn
    · exact gcd_div_gcd_div_gcd_of_pos_left (zero_lt_of_ne_zero hm)
    · exact gcd_div_gcd_div_gcd_of_pos_right (zero_lt_of_ne_zero hn)
  have pow_eq : a ^ m' = b ^ n' := by
    conv_lhs at h => rw [show m = m' * g from (Nat.div_mul_cancel (gcd_dvd_left m n)).symm]
    conv_rhs at h => rw [show n = n' * g from (Nat.div_mul_cancel (gcd_dvd_right m n)).symm]
    rw [pow_mul, pow_mul] at h
    have : g ≠ 0 := by
      rcases hmn with hm | hn
      · exact gcd_ne_zero_left hm
      · exact gcd_ne_zero_right hn
    exact Nat.pow_left_injective this h
  exact exists_eq_pow_of_exponent_coprime_of_pow_eq_pow coprime pow_eq

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

Goal state before:
pp: case pos.inl
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ c • p %ₘ q = c • (p %ₘ q)

pp: case pos.inr
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)

Tactic:
· simp only [eq_iff_true_of_subsingleton]

Goal state after:
case pos.inr
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • p %ₘ q = c • (p %ₘ q)
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)
⊢ ¬q.degree ≤ p.degree → (0, p).2.degree < q.degree

Tactic:
exact lt_of_not_ge

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ (contract p f).coeff n = f.coeff (n * p)

Tactic:
by
  simp only [contract, coeff_monomial, sum_ite_eq', finsetSum_coeff, mem_range, not_lt,
    ite_eq_left_iff]
  intro hn
  apply (coeff_eq_zero_of_natDegree_lt _).symm
  calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt

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)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f ∨ IsUnit g

Tactic:
left

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.degree = 1
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0

Tactic:
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]

Goal state after:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos.inl
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

pp: case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
· simp only [eq_iff_true_of_subsingleton]

Goal state after:
case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
rw [boundary, hnot_top, inf_bot_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
n : ℕ
s : Set M
⊢ ⇑ofAdd '' (n • s) = (⇑ofAdd '' s) ^ n

Tactic:
by
  induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
n : ℕ
s : Set (Multiplicative M)
⊢ ⇑toAdd '' s ^ n = n • ⇑toAdd '' s

Tactic:
by
  induction n with
  | zero => simp; rfl
  | succ n IH => simp [succ_nsmul, pow_succ, IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
by
  simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
    Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]

Goal state after:
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
⊢ (AddMonoidHom.mulLeft (f i)) (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
(AddMonoidHom.mulLeft (f i)).map_multiset_sum _,

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
⊢ (Multiset.map (⇑(AddMonoidHom.mulLeft (f i)))
        (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case empty
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : 1 = x * y
⊢ IsUnit x ∨ Prime x

Tactic:
left

Goal state after:
case empty
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : 1 = x * y
⊢ IsUnit x
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
obtain ⟨ha₁ | ha₂, hs⟩ := hm

Goal state after:
case cons.inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case cons.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ k ∈ {r | IsUnit r ∨ Prime r}

Tactic:
left

Goal state after:
case cons.inl.refine_1.refine_1
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit k
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}

Tactic:
left

Goal state after:
case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ IsUnit c
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y ∨ k = 0

Tactic:
left

Goal state after:
case cons.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c * s.prod = x * y
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]

Goal state after:
case cons.inr.inl.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ s.prod ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (x * c)
hc : y = c✝ * c
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]

Goal state after:
case cons.inr.inr
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c✝ : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (x * c)
hc : y = c✝ * c
⊢ s.prod ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔
    Multiset.Rel (fun x1 x2 ↦ x1 = x2) (Multiset.map Associates.mk p) (Multiset.map Associates.mk q)

Tactic:
Multiset.rel_map

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b ↦ Associates.mk a = Associates.mk b) p q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (factors a), Prime x

Tactic:
factors

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯), Prime x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
rcases eq_or_ne p 0 with rfl | hp0

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots 0 = 0 ↔ 0 = 0 ∨ IsRoot 0 = ⊥

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (factors a), normalize x = x

Tactic:
factors

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯), normalize x = x