mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (C (p.coeff 0 + a)).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree

Tactic:
heq0,

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
a : R
heq0 : p.coeff 0 = 0
x✝ : a ≠ 0
ih : 0 < p.degree → P p
h0 : 0 < (C (0 + a)).degree
h : p.degree ≤ 0
⊢ 0 < (C a).degree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f
⊢ (expand R (p * p ^ n)) f = (expand R p) ((⇑(expand R p))^[n] f)

Tactic:
expand_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n)) f = (⇑(expand R p))^[n] f
⊢ (expand R p) ((expand R (p ^ n)) f) = (expand R p) ((⇑(expand R p))^[n] f)
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]
a : R
p : R[X]
⊢ ((a • p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = a • p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
rw [sum_smul_index] <;>
      simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

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

Goal state before:

Tactic:
((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
        (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
      simp [mul_comm]
    _ = 1 := by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

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

Goal state before:
pp: case succ
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p
p : R[X]
⊢ (⇑derivative)^[k + 1] (s • p) = s • (⇑derivative)^[k + 1] p

Tactic:
simp [ih]

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
by_cases hp : p.natDegree = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (monomial (m + n - 1)) (a * (b * ↑m)) + (monomial (m + n - 1)) (a * (b * ↑n)) =
    (monomial (m - 1 + n)) (a * (b * ↑m)) + (monomial (m + (n - 1))) (a * (b * ↑n))

Tactic:
cases m with
  | zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  | succ m =>
  cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ ∃ a ∈ s, (⇑(aeval x) ∘ fun x ↦ X - C x) a = 0

Tactic:
exact ⟨x, hx, by simp⟩

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
a✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
by_cases hp : p.natDegree = 0

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
a✝ : Nontrivial R
hp : p.natDegree = 0
⊢ (p /ₘ (X - C a)).coeff n = 0

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
have : degree (p %ₘ (X - C a)) < 1 :=
    degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this : (p %ₘ (X - C a)).degree < 1
⊢ p %ₘ (X - C a) = C (eval a p)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
by_cases hp : p.natDegree = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i ↦ s i (ind i)

Tactic:
rcases hd.exists_mem_filter hS with ⟨t, htl, hd⟩

Goal state after:
α : Type u_1
I : Type u_6
l : I → Filter α
ι : I → Sort u_7
p : (i : I) → ι i → Prop
s : (i : I) → ι i → Set α
S : Set I
hd✝ : S.PairwiseDisjoint l
hS : S.Finite
h : ∀ (i : I), (l i).HasBasis (p i) (s i)
t : I → Set α
htl : ∀ (i : I), t i ∈ l i
hd : S.PairwiseDisjoint t
⊢ ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i ↦ s i (ind i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp.univ
α : Type u
s : Set (Set α)
U : Set α
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ

Tactic:
| univ =>

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

Tactic:
by_cases hp : p.natDegree = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x

Tactic:
constructor
  · intro h
    exact f.exists_antitone_basis
  · rintro ⟨x, h⟩
    rw [h.1.eq_iInf]
    exact isCountablyGenerated_seq x

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

Goal state before:
pp: ι : Sort u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i

Tactic:
refine ⟨exists_iInter_of_mem_iInf, ?_⟩
  rintro ⟨t, ht, rfl⟩
  exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ rootMultiplicity a p < n + 1

Tactic:
Nat.lt_add_one_iff

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ rootMultiplicity a p ≤ n
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (a ⊔ b)

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ b

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_5
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b))

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
exact le_sup_of_le_left inf_le_left

Goal state after:
case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s) → ∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s

Tactic:
· exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t ∈ g, ∃ x ∈ f, ∀ x_1 ∈ x, ∀ y ∈ t, m (x_1, y) ∈ s) → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ m ⁻¹' s
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x ↦ b) id) (𝓟 ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)

Tactic:
map_principal

Goal state after:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
v : α → M
i : β
h' : f ⁻¹' {i} = ∅
⊢ mapDomain f v i = 0

Tactic:
simp [mapDomain, Set.Finite.toFinset, h']

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

Goal state before:
pp: case empty
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ ∏ i ∈ ∅, f i ~ᵤ ∏ i ∈ ∅, g i

Tactic:
simp only [Finset.prod_empty]

Goal state after:
case empty
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
f g : ι → M
h : ∀ i ∈ ∅, f i ~ᵤ g i
⊢ 1 ~ᵤ 1
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case insert
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
grind [Associated.mul_mul]

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

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
⊢ Filter.TendstoCofinite fun x ↦ eval x p

Tactic:
rw [Filter.tendstoCofinite_iff_finite_preimage_singleton]
  intro x
  by_contra! hx
  obtain ⟨rfl⟩ : p = C x := p.eq_of_infinite_eval_eq (C x) (by simpa)
  simp at hp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ p, p ∈ normalizedFactors x

Tactic:
by
  obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
  obtain ⟨p, hp, _⟩ := exists_mem_normalizedFactors_of_dvd hx hp' hp'x
  exact ⟨p, hp⟩

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

Goal state before:
pp: case succ
σ : Type u_5
f g : σ →₀ ℕ
hgf : g ≤ f
IH : degree g ≤ degree f → ∃ g_1 ≤ f, degree g_1 = degree g
hn : degree g + 1 ≤ degree f
⊢ ∃ g_1 ≤ f, degree g_1 = degree g + 1

Tactic:
obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf

Goal state after:
case succ
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
⊢ ∃ g_1 ≤ g + f, degree g_1 = degree g + 1
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
f : σ →₀ ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hgf : g ≤ f
hm : degree g ∈ s
e : degree g + n = degree f
⊢ f ∈ ⇑degree ⁻¹' s + ⇑degree ⁻¹' t

Tactic:
obtain ⟨f, rfl⟩ := le_iff_exists_add.mp hgf

Goal state after:
σ : Type u_5
s t : Set ℕ
n : ℕ
hn : n ∈ t
g : σ →₀ ℕ
hm : degree g ∈ s
f : σ →₀ ℕ
hgf : g ≤ g + f
e : degree g + n = degree (g + f)
⊢ g + f ∈ ⇑degree ⁻¹' s + ⇑degree ⁻¹' t
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X - C b).roots = {↑a⁻¹ * b}

Tactic:
by
  rw [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
    Units.inv_mul, C_1, one_mul]
  exact roots_X_sub_C (a⁻¹ * b)

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Tactic:
by
  constructor
  · rintro ⟨c, rfl⟩
    simp [hx, right_ne_zero_of_mul hy]
  · rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
⊢ IsUnit r

Tactic:
suffices ¬IsUnit q by simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
⊢ ¬IsUnit q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p = q

Tactic:
rw [← sub_eq_zero]
  apply zero_of_eval_zero
  intro x
  rw [eval_sub, sub_eq_zero, ext]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
by
  rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Infinite R
⊢ f = 0

Tactic:
exact zero_of_eval_zero _ hf

Goal state after:
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
cne0 : c ≠ 0
hdeg : ¬c.natDegree = 0
⊢ ↑a.degree < ↑(a.degree + ↑c.natDegree)

Tactic:
rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]

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
hdeg : ¬c.natDegree = 0
⊢ a.natDegree < a.natDegree + c.natDegree
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
inst✝¹ : WfDvdMonoid R
f : R[X]
inst✝ : Nontrivial R
hf : 0 < f.natDegree
⊢ 0 < f.degree

Tactic:
by
    contrapose! hf
    exact natDegree_le_of_degree_le hf

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p.content ∣ q.content ∧ p.primPart ∣ q.primPart → p ∣ q

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ p ∣ q
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Tactic:
prod_normalizedFactors_eq,

Goal state after:
case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ C a.leadingCoeff * normalize a = a

case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ a ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
by simp [Polynomial.Monic.def, hq]

Goal state after:
Module: Mathlib.Algebra.Azumaya.Defs

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (r • ab) • a = r • ab • a

Tactic:
change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module (A ⊗[R] Aᵐᵒᵖ) A := Algebra.module
r : R
ab : A ⊗[R] Aᵐᵒᵖ
a : A
⊢ (Algebra.moduleAux (r • ab)) a = r • (Algebra.moduleAux ab) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : k = 0
⊢ ∃ d, a = d ^ k

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
⊢ ∃ d, a = d ^ k

Tactic:
· use 1
    rw [hk0, pow_zero] at h ⊢
    apply (mul_eq_one.1 h).1

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
⊢ ∃ d, a = d ^ k
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
x : A
⊢ IsAlgebraic R x ↔ ¬Function.Injective ⇑(aeval x)

Tactic:
by
  simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]

Goal state after:
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
n : ℤ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_intCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Int.cast n)

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
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
b : B
⊢ IsAlgebraic S b

Tactic:
obtain ⟨a, rfl⟩ := hg b

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
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
inst✝ : Algebra.IsAlgebraic R A
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
a : A
⊢ IsAlgebraic S (g a)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
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)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hx

Goal state after:
case a.refine_1
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)))
⊢ ∀ x ∈ ⇑includeLeft '' ↑I, ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

case a.refine_2
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)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = 0

case a.refine_3
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)))
⊢ ∀ (x y : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
      y ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
        (∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x) →
          (∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = y) →
            ∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = x + y

case a.refine_4
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 x : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
      (∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x) →
        ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = a • x
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

Tactic:
by
  obtain ⟨S, h⟩ := exists_finsupp_left x
  use S.graph
  rw [h, Finsupp.sum]
  apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst <;> simp

Goal state after: