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

Goal state before:
pp: α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f

Tactic:
by
  rw [sInter_eq_biInter, biInter_mem hfin]

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
I_fin : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
hU : ⋂ i, V i ⊆ U
⊢ U ∈ ⨅ i, s i

Tactic:
have := I_fin.fintype
  refine mem_of_superset (iInter_mem.2 fun i => ?_) hU
  exact mem_iInf_of_mem (i : ι) (hV _)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p * q %ₘ q = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq]
  exact dvd_mul_left q p

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
i : ↑I
⊢ ∀ U ∈ σ i, U ∈ s ↑i

Tactic:
apply σsub

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative)^[n + 1 + 1 + 2] p * X ^ 2 + (2 * (n + 1 + 1)) • (⇑derivative)^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative)^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative)^[n + 1 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
by
    simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
    ring

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ ⊤ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂)

Tactic:
simp [prod_inf_prod]

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

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

Tactic:
have := Classical.decEq α

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∃ p, a ~ᵤ p ∧ f = {p}

Tactic:
have := Classical.decEq α

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
⊢ ∃ p, a ~ᵤ p ∧ f = {p}
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ degree f = ∑ i, f i

Tactic:
rw [degree_apply, Finset.sum_subset]

Goal state after:
case h
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ f.support ⊆ Finset.univ

case hf
σ : Type u_1
R : Type u_4
inst✝¹ : AddCommMonoid R
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∀ x ∈ Finset.univ, x ∉ f.support → f x = 0
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
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Tactic:
have h : (normalize : α → α) = Associates.out ∘ Associates.mk := by
    ext
    rw [Function.comp_apply, Associates.out_mk]
  rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
    Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_add, h, ←
    Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]
  refine congr rfl ?_
  apply Multiset.map_mk_eq_map_mk_of_rel
  apply factors_unique
  · intro x hx
    rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx
  · exact irreducible_of_normalized_factor
  · rw [Multiset.prod_add]
    exact
      ((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i ↦ (f i).roots

Tactic:
rcases s with ⟨m, hm⟩

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : m.Nodup
⊢ { val := m, nodup := hm }.prod f ≠ 0 →
    ({ val := m, nodup := hm }.prod f).roots = { val := m, nodup := hm }.val.bind fun i ↦ (f i).roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ m = 0

Tactic:
refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
x : α
hx : x ∈ m
⊢ False
Module: Mathlib.RingTheory.Polynomial.Content

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

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

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

Goal state before:
pp: case refine_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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
by_cases h : b = 0

Goal state after:
case pos
α : 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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

case neg
α : 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
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t (m.choose 0 • ((⇑derivative)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0

Tactic:
· rw [m.choose_zero_right, one_smul, eval_mul, m.sub_zero, iterate_derivative_X_sub_pow_self,
      eval_natCast, nsmul_eq_mul]; rfl

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∀ b ∈ range m.succ,
    b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
⊢ a ≈ b → (fun x ↦ ↑(factors' a)) ≍ fun x ↦ ↑(factors' b)

Tactic:
hab

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Associates α
h : ¬a✝ = 0
a b : α
hab : a ≈ b
⊢ (fun x ↦ ↑(factors' a)) ≍ fun x ↦ ↑(factors' b)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart.eraseLead * p.primPart).content q.primPart.leadingCoeff *
      gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

Tactic:
(ih ..).gcd_eq_left,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart.eraseLead.content * p.primPart.content) q.primPart.leadingCoeff *
      gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (p.primPart.eraseLead * q.primPart).content p.primPart.leadingCoeff ∣ 1

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n

Tactic:
(ih ..).gcd_eq_left,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (p.primPart.eraseLead.content * q.primPart.content) p.primPart.leadingCoeff ∣ 1

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ ¬q.primPart = 0

Tactic:
apply q.primPart_ne_zero

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
⊢ Fintype G

Tactic:
let y : Associates D[X] := Associates.mk f

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y : Associates D[X] := Associates.mk f
⊢ Fintype G
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).factors = k • ↑u

Tactic:
factors_mk a0 hz,

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
⊢ ↑(factors' a0) = k • ↑u
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
⊢ Transcendental R x ↔ RingHom.ker (aeval x) = ⊥

Tactic:
rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
halg : IsAlgebraic (↥⊥) x
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Tactic:
exact ⟨r, rfl⟩

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Tactic:
exact ⟨r, rfl⟩

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

Tactic:
← divX_mul_X_add p

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 * X + C (p.coeff 0))
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_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
| (aeval x) p

Tactic:
← divX_mul_X_add p

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_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
| (aeval x) (p.divX * X + C (p.coeff 0))
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
inst✝ : Small.{u, u_1} R
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(span R (Set.range s))

Tactic:
← Fintype.range_linearCombination

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
n : ℕ
s : Fin n → M
⊢ Small.{u, u_2} ↥(Fintype.linearCombination R s).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case add
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 y : M ⊗[R] N
hx : ∃ k m n, x = ∑ j, m j ⊗ₜ[R] n j
hy : ∃ k m n, y = ∑ j, m j ⊗ₜ[R] n j
⊢ ∃ k m n, x + y = ∑ j, m j ⊗ₜ[R] n j

Tactic:
obtain ⟨kx, mx, nx, rfl⟩ := hx
    obtain ⟨ky, my, ny, rfl⟩ := hy
    use kx + ky, Fin.addCases mx my, Fin.addCases nx ny
    simp [Fin.sum_univ_add]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)

Tactic:
exact _root_.rTensor_exact M (fun x ↦ by simp [π]) Quotient.mk''_surjective

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ x ∈ Set.range ⇑0

Tactic:
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ 0 = x
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0

Tactic:
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ 0 = x
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ (t \ s).dens + s.dens = t.dens

Tactic:
simp [dens, ← card_sdiff_add_card_eq_card h, add_div]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : NegZeroClass α
hf : Function.Odd f
⊢ f 0 = 0

Tactic:
simp [← neg_eq_self, ← hf 0]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
cons_eq_insert

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ x ∈ (insert a s).powerset, f x = (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset.attach, f (insert a ↑x)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ ∀ (s : S) (n : N), g₁ n = g₂ n → g₁ (s • n) = g₂ (s • n)

Tactic:
intro s n e'
    rw [g₁.map_smul, g₂.map_smul, e']

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ s.sym (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine_2 i)

pp: case refine_2
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (a : Fin (n + 1)) → ↥(s.sym (n - ↑a)) → Sym α (n - ↑(id a))

pp: case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id ?refine_2
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id ?refine_2 ⟨i, ⟨m, hm⟩⟩

Tactic:
· exact Subtype.coe_injective

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ Sigma.map id (fun i a ↦ ↑a)
      ((fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
        ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩)) =
    Sigma.map id (fun i a ↦ ↑a) ⟨i, ⟨m, hm⟩⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
convert! mem_mk_right a <| Mem.other h

Goal state after:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ z = s(a, Mem.other h)