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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ Function.Injective ⇑((MulDistribMulAction.toMonoidEnd H G) h)

Tactic:
by intro a b; simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ Function.Injective ⇑((DistribMulAction.toAddMonoidEnd H G) h)

Tactic:
by intro a b; simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
this : if Even n.succ.succ then ∑ i ∈ range n.succ.succ, x ^ i < 0 else 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
split_ifs at this

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : Even n.succ.succ
this : ∑ i ∈ range n.succ.succ, x ^ i < 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : ¬Even n.succ.succ
this : 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
⊢ a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

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

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (k + m).choose k ≤ (k + m + 1 - k) ^ k

Tactic:
Nat.add_comm k m,

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + k + 1 - k) ^ k
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b ∈ {0, 1, 2, 3, 4} ↔
    (a, b) ∈
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
  aesop

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

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val

pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
· cases hb; simp

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a b : α
⊢ emultiplicity (f a) (f b) = emultiplicity a b

Tactic:
by
  simp [emultiplicity_eq_emultiplicity_iff, ← map_pow, map_dvd_iff]

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.factorization = single p 1

Tactic:
ext q

Goal state after:
p : ℕ
hp : Prime p
q : ℕ
⊢ p.factorization q = (single p 1) q
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
ext q

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ (a * b).factorization q = (a.factorization + b.factorization) q
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ minimalPeriod (fun x_1 ↦ x * x_1) 1 = minimalPeriod (fun x ↦ y * x) 1

Tactic:
orderOf

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

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

Tactic:
ext q

Goal state after:
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) + k.factorization p ≤ n

Tactic:
factorization_eq_card_pow_dvd_of_lt hp
      hk0.bot_lt (lt_of_le_of_lt hkn <| Nat.pow_lt_pow_succ hp.one_lt),

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
hdisj : _root_.Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})
⊢ #({i ∈ Ico 1 (log p (p ^ n)).succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) + #({i ∈ Ico 1 (n + 1) | p ^ i ∣ k}) ≤ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
⊢ d ∣ n

Tactic:
rw [dvd_iff_le_div_mul n d]

Goal state after:
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
⊢ n ≤ n / d * d
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : ((n / d).factorization + d.factorization) p < n.factorization p
⊢ False

Tactic:
add_apply,

Goal state after:
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : (n / d).factorization p + d.factorization p < n.factorization p
⊢ False
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
⊢ a ∣ b

Tactic:
if pb : b.Prime then ?_ else simpa [pb] using h b

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
⊢ 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 ≤ emultiplicity p n !

Tactic:
pow_dvd_iff_le_emultiplicity

Goal state after:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ ↑r ≤ emultiplicity p n ! ↔ ↑r ≤ emultiplicity p n !
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x : G
⊢ IsOfFinOrder x

Tactic:
by
  by_contra h; exact infinite_not_isOfFinOrder h <| Set.toFinite _

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x
  refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩
  rw [zpow_natCast]
  exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

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

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ a.factorization p = b.factorization p

pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p

Tactic:
· simp [factorization_def, pp, h p pp]

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ a.factorization p = b.factorization p
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
⊢ of' k G a /ᵒᶠ a = 1

Tactic:
by
  simpa only [one_mul] using mul_of'_divOf (1 : k[G]) a

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w✝ : R
⊢ (algebraMap R S) (eval w✝ p) ≠ 0

Tactic:
exact fun heq ↦ hp.not_isRoot_of_natDegree_ne_one hdeg <|
    FaithfulSMul.algebraMap_injective _ _ <| map_zero (algebraMap R S) ▸ heq

Goal state after:
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
hp : p ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
have hq : q ≠ 0 := right_ne_zero_of_mul hpq

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
rw [← nsmul_eq_mul', smul_eq_zero]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
hp : natDegree 0 ≠ 0
⊢ False

Tactic:
simp at hp

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

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

Tactic:
rw [hp m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2

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

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) → t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
rintro ⟨I, hIf, hpI, hst⟩
    rw [biInter_eq_iInter] at hst
    refine mem_iInf_of_iInter hIf (fun i ↦ ?_) hst
    simp [hpI i i.2]

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

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

Tactic:
· 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.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i

Tactic:
have := hs.to_subtype
  rw [biInter_eq_iInter, biInter_eq_iInter]
  exact .iInter fun i ↦ hle i.1 i.2

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
t : Set β
f : Filter α
s : Set (α × β)
u : Set α
h : u ⊆ {a | ∀ b ∈ t, (a, b) ∈ s}
x : α
y : β
hx : (x, y).1 ∈ u
hy : (x, y).2 ∈ t
⊢ (x, y) ∈ s

Tactic:
exact h hx y hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ comap Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)

Tactic:
← map_swap_eq_comap_swap

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map Prod.swap (g ×ˢ f) = map Prod.swap (g ×ˢ f)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s

Tactic:
rwa [prod_image_image_eq, image_subset_iff]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
iR : DecidableEq R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
obtain rfl := Subsingleton.elim iR (Classical.decEq R)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hp : (C x).natDegree ≠ 0
hx : ((fun x_1 ↦ eval x_1 (C x)) ⁻¹' {x}).Infinite
⊢ False

Tactic:
simp at hp

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.Algebra.Polynomial.Roots

Goal state before:
pp: n : ℕ
R : Type u_1
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ (nthRoots n a).toFinset = (nthRoots n a).toFinset

Tactic:
convert! rfl

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

Goal state before:
pp: case neg.calc_1
α : 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
cne0 : c ≠ 0
con : Classical.choose ⋯ = 0
⊢ c ~ᵤ 1

pp: case neg.calc_2
α : 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
cne0 : c ≠ 0
⊢ ∀ x ∈ Classical.choose ⋯ + Classical.choose ⋯, Prime x

pp: case neg.calc_3
α : 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
cne0 : c ≠ 0
⊢ (Classical.choose ⋯ + Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
· convert! (Classical.choose_spec (pf c cne0)).2.symm
        rw [con, Multiset.prod_zero]

Goal state after:
case neg.calc_2
α : 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
cne0 : c ≠ 0
⊢ ∀ x ∈ Classical.choose ⋯ + Classical.choose ⋯, Prime x

case neg.calc_3
α : 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
cne0 : c ≠ 0
⊢ (Classical.choose ⋯ + Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset

Tactic:
convert! rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0

Tactic:
@eq_comm _ a.factors,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, ↑s = a.factors) ↔ a ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ p % q = p

Tactic:
rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (p.divModByMonicAux ⋯).2 = p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0

Tactic:
hα,

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ 0 * eval₂ ϕ α p = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0

Tactic:
hα,

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ 0 * eval₂ ϕ α p = 0
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case right
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.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ C (c.coeff c.natDegree) = C (c.coeff 0)

Tactic:
Polynomial.natDegree_eq_of_degree_eq_some hdeg

Goal state after:
case right
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.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ C (c.coeff 0) = C (c.coeff 0)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : p ≠ 0
⊢ (normalize p).Monic

Tactic:
rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0
  rw [Monic, leadingCoeff_normalize, normalize_eq_one]
  apply hp0

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R A : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ #{ x // IsAlgebraic R x } ≤ max #R ℵ₀

Tactic:
by
  rw [← lift_id #_, ← lift_id #R]
  exact cardinalMk_lift_le_max R A

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

Goal state before:
pp: case h
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ Associates.mk a0 = FactorSet.prod ↑u ^ k

Tactic:
apply eq_of_factors_eq_factors

Goal state after:
case h
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ (Associates.mk a0).factors = (FactorSet.prod ↑u ^ k).factors
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_1
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi : i⁺ ∈ s
⊢ e₁ ⟨i⁺, hi⟩ = e₂ ⟨i⁺, hi⟩

Tactic:
ext x ⟨j, hj⟩
    obtain rfl | hj := ((lt_succ_iff_of_not_isMax nmax).mp hj).eq_or_lt
    · exact (compat₁ _ nmax x).trans (compat₂ _ nmax x).symm
    have hi : i ∈ s := hs (le_succ i) hi
    rw [piLTProj_intro (f := e₁ _ x) (le_succ i) (by exact hj),
        ← nat₁ _ hi (by exact le_succ i), ih, nat₂ _ hi (by exact le_succ i)]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(lTensor P g' ∘ₗ rTensor N' g)

Tactic:
coe_comp

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ x✝ : { P // Small.{u, u_2} ↥P }
hPR : ↑x✝² ≤ ↑x✝
hQR : ↑x✝¹ ≤ ↑x✝
⊢ ↑⟨↑x✝² ⊔ ↑x✝¹, ⋯⟩ ≤ ↑x✝

Tactic:
exact sup_le hPR hQR

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
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : Q ⊗[R] N), (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) x = (lTensor Q f).range.mkQ x

Tactic:
intro y

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
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (lTensor Q f).range.mkQ y