mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case neg
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
j : ι
hj : j ∈ s
hij : ¬i = j
⊢ (Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) =
    (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)

Tactic:
· simp [hij]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
P : R[X]
h : P.degree < ↑k
⊢ (⇑derivative)^[k] P = 0

Tactic:
by
  induction k generalizing P
  case zero => exact degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h
  case succ k ind =>
    by_cases P = 0
    case pos hP => simp [hP]
    case neg hP =>
      rw [Function.iterate_add_apply, Function.iterate_one]
      by_cases derivative P = 0
      case pos hP' => simp [hP']
      case neg hP' =>
        have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
        refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
        linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

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

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

Tactic:
Multiset.prod_cons

Goal state after:
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s✝ : Multiset M₀
a : M₀
s : Multiset M₀
ih : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
hs : ∀ r ∈ a ::ₘ s, Prime r
hps : p ∣ a * s.prod
⊢ ∃ q ∈ a ::ₘ s, p ~ᵤ q
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
      nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0

Tactic:
exact eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)

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

Goal state before:
pp: case cons
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ (a ::ₘ s).prod ∣ n

Tactic:
Multiset.prod_cons

Goal state after:
case cons
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a * s.prod ∣ n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ normalizedFactors b).prod

Tactic:
Multiset.prod_cons

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ rootMultiplicity s (X - C r) = count s {r}

Tactic:
rootMultiplicity_X_sub_C,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ (if s = r then 1 else 0) = count s {r}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ (p ::ₘ fx).prod ~ᵤ p * x

Tactic:
Multiset.prod_cons

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ p * fx.prod ~ᵤ p * x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 0 r = 0

Tactic:
simp only [pow_zero, nthRoots, ← C_1, ← C_sub, roots_C]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
intro s t hs ht eq

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
h₁ : X ^ 2 - C 1 = (X + C 1) * (X - C 1)
h : X ^ 2 - C 1 = 0
⊢ False

Tactic:
by simpa using congrArg (coeff · 0) h

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

Goal state before:
pp: case succ.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff b = 0

Tactic:
apply h1

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

Goal state before:
pp: case h₁
α : 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 ~ᵤ a

Tactic:
apply (Classical.choose_spec (pf _ _)).2

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 ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h₂
α : 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 ~ᵤ c

Tactic:
apply (Classical.choose_spec (pf _ _)).2

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
⊢ c ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
x✝ : R
⊢ x✝ ∈ (fun x ↦ eval x p) ⁻¹' {a} ↔ x✝ ∈ (p - C a).rootSet R

Tactic:
simp [mem_rootSet_of_ne (sub_ne_zero.mpr hp), sub_eq_zero]

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

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

Tactic:
intro q q_dvd_pa' q_dvd_b'

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
⊢ IsUnit q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ ↑1! ∈ nonZeroDivisors R

Tactic:
rw [Nat.factorial_one, Nat.cast_one]; exact Submonoid.one_mem _

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity (f a) (map f p)

Tactic:
rw [le_rootMultiplicity_iff hmap]
  refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))
  rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]

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

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ map f (p / q) = map f p / map f q

Tactic:
if hq0 : q = 0 then simp [hq0]
  else
    rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
      Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Goal state after:
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

pp: case neg
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:
case neg
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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ⊓ Associates.mk b

Tactic:
le_inf_iff,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ∧ Associates.mk a ≤ Associates.mk b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ⊓ Associates.mk b

Tactic:
le_inf_iff,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ Associates.mk a ≤ Associates.mk c ∧ Associates.mk a ≤ Associates.mk b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p : R[X]
⊢ p / C a = p * C a⁻¹

Tactic:
by
  simpa [mul_comm] using div_C_mul (q := 1)

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

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors

Tactic:
· apply Or.intro_left
    rw [hb0, add_zero]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ p₁ %ₘ (q * C q.leadingCoeff⁻¹) = p₂ %ₘ (q * C q.leadingCoeff⁻¹)

Tactic:
apply Polynomial.modByMonic_eq_of_dvd_sub (by simp [Polynomial.Monic.def, hq])

Goal state after:
case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ q * C q.leadingCoeff⁻¹ ∣ p₁ - p₂
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ 0 = q.count (p ^ n).factors

Tactic:
symm

Goal state after:
case e'_4
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ q.count (p ^ n).factors = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ p ^ p.count a.factors = a

Tactic:
symm

Goal state after:
case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ p.count a.factors
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
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a

Tactic:
Transcendental,

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ ¬IsAlgebraic R ((algebraMap S A) a) ↔ ¬IsAlgebraic R a
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 ι
z w : DirectLimit G f
i : ι
x : G i
hx : (of R ι G f i) x = z
j : ι
y : G j
hy : (of R ι G f j) y = w
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of R ι G f k) ((f i k hik) x) = z

Tactic:
rw [of_f, hx]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
hfg : Exact ⇑f ⇑g
⊢ (lTensor Q f).range ≤ (lTensor Q g).ker

Tactic:
rw [LinearMap.range_le_iff_comap, ← LinearMap.ker_comp,
      ← lTensor_comp, hfg.linearMap_comp_eq_zero, lTensor_zero, ker_zero]

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

Goal state before:
pp: case a.refine_4.tmul.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx✝ : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hy :
  ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y)

Tactic:
obtain ⟨x', hx'⟩ := hx

Goal state after:
case a.refine_4.tmul.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
a : A
b : B
x y : ↥(Submodule.restrictScalars R I) ⊗[R] B
hy :
  ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y
x' : ↥(Submodule.restrictScalars R I) ⊗[R] B
hx' :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x' =
    a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y_1,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 =
      a ⊗ₜ[R] b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) (x + y)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ⊗ₜ[R] 1 ∈ map includeLeft I

Tactic:
apply Ideal.mem_map_of_mem includeLeft

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
a : ↥(Submodule.restrictScalars R I)
b : B
this : ↑a ⊗ₜ[R] b = 1 ⊗ₜ[R] b * ↑a ⊗ₜ[R] 1
⊢ ↑a ∈ I