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

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 ↦ x * x_1
⊢ Nat.find h1 = n ↔ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 ↦ x * x_1) m 1

Tactic:
rw [find_eq_iff]
    simp only [h, true_and, not_and]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
rw [hb, ← mul_assoc] at ha

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred.succ * y)

Tactic:
_root_.pow_succ,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf (x ^ (orderOf x).pred * x * y)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
by
  by_cases h0 : orderOf x = 0
  · rw [h0, lcm_zero_left]
    apply dvd_zero
  conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]
  exact
    (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
      (Nat.lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (Nat.dvd_lcm_left _ _), Nat.dvd_lcm_right _ _⟩)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y

Tactic:
have hoy := hy.orderOf_pos

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
⊢ orderOf (x * y) = orderOf y
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
⊢ (a / p ^ a.factorization p).factorization ≤ (b / p ^ b.factorization p).factorization

Tactic:
factorization_ordCompl a 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 ≤ (b / p ^ b.factorization p).factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
intro e

Goal state after:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
⊢ e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
obtain _ | hprime := hR
  · simp only [pow_one]
  · let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
    simp [hr]

Goal state after:
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
g : G
⊢ 0 /ᵒᶠ g = 0

Tactic:
ext; simp

Goal state after:
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
x : k[G]
⊢ x /ᵒᶠ 0 = x

Tactic:
ext; simp

Goal state after:
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
x y : k[G]
g : G
⊢ (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n % ↑(Nat.card G)) = a ^ n

Tactic:
by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ degree 0 < (0 * X + C ((C (p.coeff 0)).coeff 0)).degree

Tactic:
degree_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ⊥ < (0 * X + C ((C (p.coeff 0)).coeff 0)).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ f.coeff 0 = 0

Tactic:
rw [hfg, coeff_X_mul_zero]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
modByMonic_eq_of_not_monic p hq

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ p.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
⊢ p.degree < q.degree

Tactic:
have := modByMonic_add_div p q

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ degree 0 < p.degree

Tactic:
degree_zero,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ ⊥ < p.degree
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ S.val ((aeval x) p) = 0

Tactic:
rw [← aeval_algHom_apply, S.val_apply]

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

Goal state before:
pp: case inr.refine_1.e_a.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p x✝¹ x✝ : R[X]
⊢ Finsupp.onFinset (range ((x✝¹ + x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ + x✝)) ⋯ =
    Finsupp.onFinset (range (x✝¹.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝¹) ⋯ +
      Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x✝¹ : R
x✝ : R[X]
⊢ Finsupp.onFinset (range ((x✝¹ • x✝).natDegree + 1)) (fun x ↦ (⇑derivative)^[x] (x✝¹ • x✝)) ⋯ =
    (RingHom.id R) x✝¹ • Finsupp.onFinset (range (x✝.natDegree + 1)) (fun x ↦ (⇑derivative)^[x] x✝) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ a ∈ (comap m f).ker ↔ a ∈ m ⁻¹' f.ker

Tactic:
simp only [mem_ker, mem_comap, forall_exists_index, and_imp, @forall_comm (Set α), mem_preimage]

Goal state after:
α : Type u_2
β : Type u_3
m : α → β
f : Filter β
a : α
⊢ (∀ b ∈ f, ∀ (a_1 : Set α), m ⁻¹' b ⊆ a_1 → a ∈ a_1) ↔ ∀ s ∈ f, m a ∈ s
Module: Mathlib.Order.Filter.Ker

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

Tactic:
by
  rw [← sSup_pair, ker_sSup, biUnion_pair]

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i : Set ι × (ι → κ)),
    (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) →
      ∃ i', (i'.1.Finite ∧ p i'.2) ∧ (i'.1.pi fun i ↦ s i i'.2) ⊆ i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)

Tactic:
rintro ⟨I, k⟩ ⟨hI, hk⟩
    rcases h_dir I k hI hk with ⟨k₀, hk₀, hk₀'⟩
    exact ⟨⟨I, k₀⟩, ⟨hI, hk₀⟩, Set.pi_mono hk₀'⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
l : (i : ι) → Filter (β i)
⊢ (pi fun i ↦ comap (f i) (l i)) = comap (Pi.map f) (pi l)

Tactic:
simp [Filter.pi, Filter.comap_comap, Function.comp_def]

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

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

Tactic:
by
  simp only [prod_eq_inf, comap_comap, Function.comp_def, inf_comm, Prod.swap, comap_inf]

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

Goal state before:
pp: case refine_4.refine_3
α : 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
⊢ Coheyting.boundary f ≤ q.2

Tactic:
grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]
      exact Coheyting.boundary_le

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∑ T ∈ powersetCard (#S - k) S, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) =
    ∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)

Tactic:
rw [← sum_finset_product']
        grind

Goal state after:
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 : Multiset.prod 0 = x * y
⊢ IsUnit x ∨ Prime x

Tactic:
simp only [Multiset.prod_zero] at hprod

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 ∨ Prime x
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

Tactic:
exact .of_mul_eq_one _ hprod.symm

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)) =
    ∑ T ∈ powersetCard (#S - (k + 1)) S, ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a)

Tactic:
rw [← sum_finset_product']
        grind

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
x : R
w : p ≠ 0
⊢ x ∈ p.roots ↔ (aeval x) p = 0

Tactic:
rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w,
    Algebra.algebraMap_self, map_id]

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
τ : Type u_5
f : σ → τ
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : CanonicallyOrderedAdd M
x : τ →₀ M
hf : Set.InjOn f (f ⁻¹' ↑x.support)
⊢ degree (comapDomain f x hf) ≤ degree x

Tactic:
by
  classical
  simpa [degree, comapDomain, Finset.sum_preimage' f x.support hf x] using
    Finset.sum_le_sum_of_subset (Finset.filter_subset ..)

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

Goal state before:
pp: α : 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 ⋯).prod * (Classical.choose ⋯).prod ~ᵤ a * c

pp: α : 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
⊢ a * c ~ᵤ (Classical.choose ⋯).prod

Tactic:
· apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption

Goal state after:
α : 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
⊢ a * c ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
| p.content

Tactic:
rw [p.eq_C_content_mul_primPart]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
| (C p.content * p.primPart).content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b
      refine ⟨p * a', b', c', ?_, mul_left_comm _ _ _, rfl⟩
      intro q q_dvd_pa' q_dvd_b'
      rcases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q | q_dvd_a'
      · have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
        contradiction
      exact coprime q_dvd_a' q_dvd_b'

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
⊢ a ≠ 0

Tactic:
apply ha0

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

Goal state before:
pp: α : 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) ⊓ (Associates.mk b).factors ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

Tactic:
factors_mk b hb,

Goal state after:
α : 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, Prime p ∧ p ∣ a ∧ p ∣ b
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

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

Tactic:
have cne0 : c ≠ 0 := right_ne_zero_of_mul hac

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Field R
⊢ C (a / b) = C a / C b

Tactic:
rw [div_C, ← C_mul, div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
k : ℕ
⊢ (a ^ k).factors = k • a.factors

Tactic:
induction k with
  | zero => rw [zero_nsmul, pow_zero]; exact factors_one
  | succ n h => rw [pow_succ, succ_nsmul, factors_mul, h]

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ p.count m.factors ≠ 0 → p ≤ m

Tactic:
rw [← pos_iff_ne_zero]

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ 0 < p.count m.factors → p ≤ m
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
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ (aeval ⟨s, ⋯⟩).toRingHom r = ⟨(aeval s) r, ht⟩

Tactic:
ext; simp

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0

Tactic:
· rw [map_add, map_mul, aeval_X, aeval_C]

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toDirectLimit f M ∘ₗ fromDirectLimit f M = LinearMap.id

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ fromDirectLimit f M ∘ₗ toDirectLimit f M = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
⊢ lift R ι G f (fun i ↦ F ∘ₗ of R ι G f i) ⋯ = F

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
⊢ lift R ι G f (of R ι G f) ⋯ = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
⊢ map (fun x ↦ LinearMap.id) ⋯ = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommMonoid (G i)
inst✝⁵ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁴ : DecidableEq ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
⊢ map g₂ hg₂ ∘ₗ map g₁ hg₁ = map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
⊢ lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯ = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
⊢ Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯ = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
⊢ lift G f P (fun i ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext; simp

Goal state after: