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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ.succ, n.succ.choose k • ((⇑derivative)^[n.succ - k] p * (⇑derivative)^[k] q)

Tactic:
rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊓ g).IsCountablyGenerated

Tactic:
rcases g.exists_antitone_basis with ⟨t, ht⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊓ g).IsCountablyGenerated
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
⊢ (f ⊔ g).IsCountablyGenerated

Tactic:
rcases g.exists_antitone_basis with ⟨t, ht⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Sort u_5
f g : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : g.IsCountablyGenerated
s : ℕ → Set α
hs : f.HasAntitoneBasis s
t : ℕ → Set α
ht : g.HasAntitoneBasis t
⊢ (f ⊔ g).IsCountablyGenerated
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: α : Type u_2
a : α
⊢ (pure a).ker = {a}

Tactic:
by rw [← principal_singleton, ker_principal]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
apply Polynomial.modByMonic_eq_of_dvd_sub h

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
· rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]
    exact ⟨p.natTrailingDegree,
      fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt_add_one _⟩

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case e'_3.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0] p * X + 0 • (⇑derivative)^[0 - 1] p =
    ∑ k ∈ range (min 1 0).succ, (Nat.choose 0 k * Nat.descFactorial 1 k) • ((⇑derivative)^[0 - k] p * X ^ (1 - k))

Tactic:
simp [sum_range_succ]

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

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

Tactic:
simp [sum_range_succ]

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

Goal state before:
pp: case e'_3.zero
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ (⇑derivative)^[0 + 1] p * X + 0 • (⇑derivative)^[0] p =
    ∑ k ∈ range (min 1 0).succ,
      (Nat.choose 0 k * Nat.descFactorial 1 k) • ((⇑derivative)^[0 - k] (derivative p) * X ^ (1 - k))

Tactic:
simp [sum_range_succ]

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

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

Tactic:
simp [sum_range_succ]

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
⊢ (a ∧ b ∨ ¬(a ∧ b)) ∧ ((a ∨ b) ∨ ¬(a ∨ b)) → a ∨ ¬a

Tactic:
rintro ⟨⟨ha, _⟩ | hnab, (ha | hb) | hnab⟩

Goal state after:
case inl.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha✝ : a
right✝ : b
ha : a
⊢ a ∨ ¬a

case inl.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ hb : b
⊢ a ∨ ¬a

case inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
ha : a
right✝ : b
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a

case inr.inl.inl
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
ha : a
⊢ a ∨ ¬a

case inr.inl.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab : ¬(a ∧ b)
hb : b
⊢ a ∨ ¬a

case inr.inr
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b✝ : α
a b : Prop
hnab✝ : ¬(a ∧ b)
hnab : ¬(a ∨ b)
⊢ a ∨ ¬a
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ 0 = eval₂ C q 0 * derivative q

Tactic:
eval₂_zero,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ 0 = 0 * derivative q
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ (Pi.map f '' (I, s).1.pi fun i ↦ id ((I, s).2 i)) ∈ pi fun i ↦ map (f i) (l i)

Tactic:
classical
  rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
  refine univ_pi_mem_pi (fun i ↦ ?_) ?_
  · by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]
  · filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
    simp [hiI, hsurj.range_eq]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, Prime x

Tactic:
rw [normalizedFactors, factors]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯), Prime x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯), Prime x

Tactic:
split_ifs with ane0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) 0, Prime x

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : ¬a = 0
⊢ ∀ x ∈ Multiset.map (fun x ↦ normalize x) (Classical.choose ⋯), Prime x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Goal state after:
case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s ≤ (weight w) f
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ normalizedFactors a, normalize x = x

Tactic:
rw [normalizedFactors, factors]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯), normalize x = x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
H : ¬x = 0
r : R
⊢ count r (C x).roots = count r 0

Tactic:
rw [count_roots, count_zero, rootMultiplicity_eq_zero (not_isRoot_C _ _ H)]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count x (Multiset.map f (p.comp (C a * X + C b)).roots) = count x p.roots

Tactic:
obtain ⟨x, rfl⟩ := hf.surjective x

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count (f x) (Multiset.map f (p.comp (C a * X + C b)).roots) = count (f x) p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p ~ᵤ q
⊢ p ∈ normalizedFactors x

Tactic:
rw [associated_iff_eq] at hqeq

Goal state after:
case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
hprime : Prime p
hdvd : p ∣ x
q : α
hqmem : q ∈ normalizedFactors x
hqeq : p = q
⊢ p ∈ normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h✝ : Subsingleton α
x✝ : α
⊢ x✝ ∉ s

Tactic:
convert! hs

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n

Tactic:
rw [mem_support_iff, Classical.not_not] at h

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ c = (factors c).prod

Tactic:
refine associated_iff_eq.mp (factors_prod fun hc => ?_).symm

Goal state after:
case refine_2.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
hc : c = 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.calc_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ ∀ x ∈ Classical.choose ⋯ + Classical.choose ⋯, Prime x

pp: case neg.calc_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯ + Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod

Tactic:
· intro x hadd
        rw [Multiset.mem_add] at hadd
        rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption

Goal state after:
case neg.calc_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯ + Classical.choose ⋯).prod ~ᵤ (Classical.choose ⋯).prod
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False

Tactic:
rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p)! ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n ! = ↑(rootMultiplicity t p)! * q
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝

Tactic:
rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq : q ≠ 0
⊢ (p %ₘ (q * C q.leadingCoeff⁻¹)).degree < q.degree

Tactic:
refine (Polynomial.degree_modByMonic_lt p ?_).trans_eq (by simp)

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq : q ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).Monic
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ IsUnit p.leadingCoeff

Tactic:
apply hp0

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

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝³ : Field R
p : R[X]
inst✝² : DecidableEq R
inst✝¹ : Field S
inst✝ : DecidableEq S
f : R →+* S
hp : ¬p = 0
⊢ map f (normalize p) = normalize (map f p)

Tactic:
simp [normalize_apply, Polynomial.map_mul, normUnit, hp]

Goal state after:
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.count a.factors ≤ Nat.find ⋯

Tactic:
· have hph := pow_ne_zero (@Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩) hp.ne_zero
    rcases subsingleton_or_nontrivial α with hα | hα
    · simp [eq_iff_true_of_subsingleton] at hph
    convert! count_le_count_of_le hph hp (@Nat.find_spec (fun n => a ∣ p ^ n) _ ⟨n, h⟩)
    rw [count_pow hp.ne_zero hp, count_self hp, mul_one]

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

Tactic:
by
  rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)

Goal state after:
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
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ (aeval s) (q - C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : s ∣ (algebraMap R S) (q.coeff 0)
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
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
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
⊢ Function.Injective ⇑(lift R ι G f g Hg)

Tactic:
cases isEmpty_or_nonempty ι
  · apply Function.injective_of_subsingleton
  intro z w eq
  obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w
  simp_rw [lift_of] at eq
  rw [injective _ eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
⊢ (lTensor Q g).range = (lTensor Q g.range.subtype).range

Tactic:
by
  have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
  nth_rewrite 1 [this]
  rw [lTensor_comp]
  apply range_comp_of_range_eq_top
  rw [range_eq_top]
  apply lTensor_surjective
  rw [← range_eq_top, range_rangeRestrict]

Goal state after:
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
ι : Type u_3
P : ι → Submodule R M
inst✝¹ : Small.{u, u_3} ι
inst✝ : ∀ (i : ι), Small.{u, u_2} ↥(P i)
⊢ Small.{u, u_2} ↥((DFinsupp.lsum ℕ) fun i ↦ (P i).subtype).range

Tactic:
apply small_range

Goal state after:
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} ↥(Fintype.linearCombination R s).range

Tactic:
apply small_range

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
s : Set S
inst✝ : Small.{u, u_2} ↑s
⊢ Small.{u, u_2} ↥(aeval Subtype.val).range

Tactic:
apply small_range

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
⊢ Exact ⇑(rTensor Q f) ⇑(rTensor Q g)

Tactic:
rw [rTensor_exact_iff_lTensor_exact]

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
ι : Type v
⊢ Flat R (ι →₀ R)

Tactic:
classical exact of_linearEquiv (finsuppLEquivDirectSum R R ι)

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

Goal state before:
pp: ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁴ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝³ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Star (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x : G i
⊢ star ⟦⟨i, x⟩⟧ = ⟦⟨i, star x⟩⟧

Tactic:
by
  rfl

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 g)

Tactic:
suffices exact1 : Function.Exact (f.rTensor M) (π.rTensor M) by
    rw [show g = ι.comp π from rfl, rTensor_comp]
    exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Goal state after:
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 π)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]

Goal state after:
case cons.h
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ j ∉ t i ∩ ⋃ x ∈ s, t x