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

Goal state before:
pp: case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (bit b n).bits

Tactic:
bits_append_bit _ _ fun hn => absurd hn h

Goal state after:
case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (b :: n.bits)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
by_cases hf : FiniteMultiplicity a b
  · rw [← ENat.natCast_zero, emultiplicity_eq_coe]
    simp
  · simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
h✝ : ¬FiniteMultiplicity a b
⊢ ⊤ ≤ if h : FiniteMultiplicity c d then ↑(Nat.find h) else ⊤

Tactic:
next h_1 =>
      simp_all only [not_exists, Decidable.not_not, not_true_eq_false, top_le_iff,
        dite_eq_right_iff, ENat.natCast_ne_top, imp_false, not_false_eq_true, implies_true]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
a b : α
h : FiniteMultiplicity a b
n : ℕ
hn : ¬a ^ (n + 1) ∣ b
hb : b = 0
⊢ False

Tactic:
simp [hb] at hn

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f x ^ n = 1

Tactic:
by rw [← f.map_pow, hn, f.map_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ 0 < orderOf x ↔ IsOfFinOrder x

Tactic:
rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization ↔ (f.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
by
  constructor <;> rintro rfl
  exacts [prod_factorization_pow_eq_self hn, prod_pow_factorization_eq_self hf |>.symm]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
this : IsUnit a
⊢ False

Tactic:
simpa [this] using ha.not_isUnit

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)) = emultiplicity p a + emultiplicity p b

Tactic:
hfin.mul_left.emultiplicity_eq_multiplicity,

Goal state after:
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) + emultiplicity p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : (p * i + r).factorization p = 0
⊢ ¬p ∣ r

Tactic:
factorization_eq_zero_iff

Goal state after:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ Nat.lcm 0 (orderOf (x * y))

Tactic:
lcm_zero_left

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
simp only [factorization_choose hp hkn (Nat.lt_add_one _), card_eq_zero, filter_eq_empty_iff,
    mem_Ico, not_le, and_imp]

Goal state after:
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ∀ ⦃x : ℕ⦄, 1 ≤ x → x < log p n + 1 → k % p ^ x + (n - k) % p ^ x < p ^ x
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ∀ ⦃x : ℕ⦄, 1 ≤ x → x < log p n + 1 → k % p ^ x + (n - k) % p ^ x < p ^ x

Tactic:
intro i hi₁ hi

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

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ a = 1

Tactic:
rw [← Nat.dvd_one, ← Nat.mul_dvd_mul_iff_left hb0.bot_lt, mul_one]

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i

Tactic:
rw [← ENat.natCast_le_natCast, ← hp.emultiplicity_factorial hbn, pow_dvd_iff_le_emultiplicity]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card (G ⧸ zpowers x) * card ↥(zpowers x)

Tactic:
← Fintype.card_prod,

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ card G = card ((G ⧸ zpowers x) × ↥(zpowers x))
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ (n % ↑(card G)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ (C (p.coeff 0)).divX = 0

Tactic:
divX_C

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ eval r x✝¹ = 0 ∨ eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0

Tactic:
exact id

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n

pp: case neg
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = f.coeff n

Tactic:
· rw [Nat.div_mul_cancel h]

Goal state after:
case neg
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = f.coeff n
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
by
  classical
  have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = ∑ i ∈ ∅, a ^ (i - (n + 1)) * p.coeff i

Tactic:
sum_empty

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
⊢ (if C r = 0 then 0 else multiplicity (X - C a) (C r)) = 0

Tactic:
split_ifs with hr

Goal state after:
case pos
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : C r = 0
⊢ 0 = 0

case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
⊢ multiplicity (X - C a) (C r) = 0
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : t ∈ ⨅ i, l i
⊢ ∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t

Tactic:
rcases (HasBasis.iInf' hl).mem_iff.mp ht with ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
ht : t ∈ ⨅ i, l i
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI : (I, f).1.Finite
hf : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ ∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: α : Type u_2
f g : Filter α
⊢ (f ⊔ g).ker = f.ker ∪ g.ker

Tactic:
rw [← sSup_pair, ker_sSup, biUnion_pair]

Goal state after:
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)).NeBot ↔ ∀ (i : ι), (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

Goal state after:
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 ι
⊢ (pi f ⊓ 𝓟 (I.pi s)).NeBot ↔ ∀ i ∈ I, (f i ⊓ 𝓟 (s i)).NeBot

Tactic:
simp [neBot_iff]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
⊢ (pi f).NeBot ↔ ∀ (i : ι), (f i).NeBot

Tactic:
simp [neBot_iff]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
S : Finset R
hk : 0 ≤ #S
⊢ (⇑derivative)^[0] (∏ a ∈ S, (X - C a)) = ↑0! * ∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, (X - C a)

pp: case succ
R : Type u
inst✝ : CommRing R
S : Finset R
n✝ : ℕ
a✝ : n✝ ≤ #S → (⇑derivative)^[n✝] (∏ a ∈ S, (X - C a)) = ↑n✝! * ∑ T ∈ powersetCard (#S - n✝) S, ∏ a ∈ T, (X - C a)
hk : n✝ + 1 ≤ #S
⊢ (⇑derivative)^[n✝ + 1] (∏ a ∈ S, (X - C a)) = ↑(n✝ + 1)! * ∑ T ∈ powersetCard (#S - (n✝ + 1)) S, ∏ a ∈ T, (X - C a)

Tactic:
case zero => simp

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
S : Finset R
n✝ : ℕ
a✝ : n✝ ≤ #S → (⇑derivative)^[n✝] (∏ a ∈ S, (X - C a)) = ↑n✝! * ∑ T ∈ powersetCard (#S - n✝) S, ∏ a ∈ T, (X - C a)
hk : n✝ + 1 ≤ #S
⊢ (⇑derivative)^[n✝ + 1] (∏ a ∈ S, (X - C a)) = ↑(n✝ + 1)! * ∑ T ∈ powersetCard (#S - (n✝ + 1)) S, ∏ a ∈ T, (X - C a)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.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₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
hc

Goal state after:
case cons.inr.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₂ : Prime c✝
c : M₀
hc : x = c✝ * c
⊢ c✝ * c ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ g.erase b)

Tactic:
exact
      Multiset.Rel.cons hb
        (ih (fun q hq => hf _ (by simp [hq]))
          (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
          (Associated.of_mul_left
            (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
            (hf p (by simp)).ne_zero))

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (Multiset.replicate (normalizedFactors r).card p).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Tactic:
Multiset.prod_replicate

Goal state after:
case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : p ^ (normalizedFactors r).card ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

Tactic:
apply Multiset.induction_on_multiset_quot p

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s).prod = q.prod → map (Quot.mk ⇑(Associated.setoid α)) s = q
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Monic
⊢ p.IsPrimitive

Tactic:
by
  rintro r ⟨q, h⟩
  exact .of_mul_eq_one (q.coeff p.natDegree) (by rwa [← coeff_C_mul, ← h])

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

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

Tactic:
rw [← normalize_content, normalize_eq_one, IsPrimitive]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ y

Tactic:
← (prod_normalizedFactors hy).dvd_iff_dvd_right

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ (normalizedFactors y).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ (∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x) → x ∣ y

pp: case mpr
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ x ∣ y → ∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x

Tactic:
· rintro ⟨s, hs, rfl⟩
    rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul,
      ← (prod_normalizedFactors hy).dvd_iff_dvd_right]
    exact Multiset.prod_dvd_prod_of_le hs

Goal state after:
case mpr
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ x ∣ y → ∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (↑a + ↑b).prod = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : (C (p.coeff 0)).degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False

Tactic:
hc

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
h : (C 0).degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hp0 : p = 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
simp only [hp0, roots_zero, Multiset.map_zero, Polynomial.map_zero, le_rfl]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → p ∣ a

Tactic:
← mk_dvd_mk

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → Associates.mk p ∣ Associates.mk a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → p ∣ a

Tactic:
← mk_dvd_mk

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → Associates.mk p ∣ Associates.mk a
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
b : R
ha : a ≠ 0
⊢ (C a * X + C b).roots = {-(a⁻¹ * b)}

Tactic:
simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

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

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

Tactic:
hc

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : ¬Associates.mk a ⊓ Associates.mk b = 1
hc : ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
⊢ False
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
⊢ IsAlgebraic R 1

Tactic:
rw [← map_one (algebraMap R A)]
  exact isAlgebraic_algebraMap 1

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental S B
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental R A

Tactic:
by
  rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
⊢ conjAlgEquiv S f = conjAlgEquiv S g ↔ ∃ α, f = α • g

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨y, h⟩ ↦ conjAlgEquiv_ext_iff.mpr ⟨(y : S), congr($h)⟩⟩

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
⊢ ∃ α, f = α • g
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
b : L
p : K[X]
hp : p ≠ 0
he : (aeval b) p = 0
f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
⊢ ∃ a, f a = b

Tactic:
obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩

Goal state after:
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
b : L
p : K[X]
hp : p ≠ 0
he : (aeval b) p = 0
f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
a : ↑(p.rootSet L)
ha : f' a = ⟨b, ⋯⟩
⊢ ∃ a, f a = b
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3.inl
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✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : (aeval x) p = 0
⊢ (↑x)⁻¹ ∈ A

pp: case refine_3.inr
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✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
· exact ih hp aeval_eq

Goal state after:
case refine_3.inr
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✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A