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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h✝ : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ (X - C x) = 0
⊢ False

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp; exact hp rfl

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ False

Tactic:
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑q.natDegree + (r - p /ₘ q).degree < ↑q.natDegree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑q.natDegree + ↑(r - p /ₘ q).natDegree < ↑q.natDegree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
I : Set ι
f : (i : ι) → ι' i
hsub : ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ⊆ t
hI₁ : (I, f).1.Finite
hI₂ : ∀ i ∈ (I, f).1, p i ((I, f).2 i)
⊢ ⋂ i ∈ (I, f).1, s i ((I, f).2 i) ∈ ⨅ i, l i

Tactic:
exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
⊢ X - C a ∣ p - C (eval a p)

Tactic:
rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
rcases hp.lt_or_gt with hd | hd

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : 0 < p.degree
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff
Module: Mathlib.Order.Filter.Prod

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

Tactic:
by
  simp only [prod_eq_inf, comap_sup, inf_sup_left]

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

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

Tactic:
· exact Or.inr fun ha => hnab <| Or.inl ha

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

Goal state before:
pp: α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ (⋃ x ∈ sᶜ, {x})ᶜ ∈ l

Tactic:
compl_iUnion₂,

Goal state after:
α : Type u_2
l : Filter α
h : ∀ (x : α), {x}ᶜ ∈ l
s : Set α
hs : sᶜ.Finite
⊢ ⋂ i ∈ sᶜ, {i}ᶜ ∈ l
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s

Tactic:
prod_image_image_eq,

Goal state after:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p ↦ (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (fun p ↦ (m₁ p.1, m₂ p.2)) '' s₁ ×ˢ s₂ ⊆ s
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_1
ι : 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
i : ι
⊢ f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i ∈ map (f i) (l i)

Tactic:
by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative ↑n = 0

Tactic:
← C_eq_intCast n

Goal state after:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ derivative (C ↑n) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ (⇑derivative)^[n] ((X - C c) ^ n) = ↑n !

Tactic:
by
  rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this : DecidableEq (Associates M)
⊢ p.prod * 1 ≤ p.prod * (q - p).prod

Tactic:
exact mul_mono (le_refl p.prod) one_le

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1

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

Goal state before:
pp: σ : Type u_5
s : Set ℕ
n : ℕ
hn : n ≠ 0
⊢ ⇑degree ⁻¹' (n • s) = n • ⇑degree ⁻¹' s

Tactic:
obtain (_ | n) := n; · contradiction
  induction n <;> simp_all [succ_nsmul, degree_preimage_add]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

Tactic:
hcases

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y

Tactic:
intro h
    exact
      dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)

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

Goal state before:
pp: T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ p.rootSet S = ↑(p.aroots S).toFinset

Tactic:
rw [rootSet]

Goal state after:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).rootSet S = ∅

Tactic:
by
  classical
  rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (-p).rootSet S = p.rootSet S

Tactic:
rw [rootSet, aroots_neg, rootSet]

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b

Tactic:
intro a a_unit _ b

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
      iff_false, not_exists]
    exact fun a => not_and_of_not_right _ a.prop.ne_zero

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

Goal state before:
pp: case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ q.roots = 0

Tactic:
replace he := congr_arg roots he.symm
    rw [roots_mul, roots_multiset_prod_X_sub_C] at he
    exacts [add_eq_left.1 he, mul_ne_zero (monic_multisetProd_X_sub_C p.roots).ne_zero hq]

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

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
⊢ False

Tactic:
by
    rw [eq_C_of_degree_le_zero h] at hp0 hp
    exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ (p * q).IsPrimitive

Tactic:
rw [isPrimitive_iff_content_eq_one, ← normalize_content, normalize_eq_one]
  refine (associated_content_mul p q).symm.isUnit ?_
  simp_rw [hp.content_eq_one, hq.content_eq_one, mul_one, isUnit_one]

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ (↑(p.aroots B).toFinset).ncard ≤ p.natDegree

Tactic:
Set.ncard_coe_finset,

Goal state after:
A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ #(p.aroots B).toFinset ≤ p.natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ Associated (p * q).primPart (p.primPart * q.primPart)

Tactic:
rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0
  refine .of_mul_left ?_ .rfl h0
  conv_lhs => rw [← (p * q).eq_C_content_mul_primPart,
    p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart, mul_mul_mul_comm, ← C_mul]
  gcongr
  exact (associated_content_mul ..).symm.map _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ↑(((monomial n) a).aroots S).toFinset = {0}

Tactic:
aroots_monomial ha,

Goal state after:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ↑(n • {0}).toFinset = {0}
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ (g ⁻¹' {f}).Countable

Tactic:
suffices MapsTo (↑) (g ⁻¹' {f}) (f.rootSet A) from
    this.countable_of_injOn Subtype.coe_injective.injOn (f.rootSet_finite A).countable

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ MapsTo Subtype.val (g ⁻¹' {f}) (f.rootSet A)
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 : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (S.sum fun m n ↦ m ⊗ₜ[R] n) = (TensorProduct.comm R M N) (S.sum fun n m ↦ m ⊗ₜ[R] n)

Tactic:
Finsupp.sum,

Goal state after:
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 : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∑ x ∈ S.support, x ⊗ₜ[R] S x = (TensorProduct.comm R M N) (∑ x ∈ S.support, S x ⊗ₜ[R] x)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case h
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 : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∑ a ∈ S.support, a ⊗ₜ[R] S a = ∑ i ∈ S.graph, i.1 ⊗ₜ[R] i.2

Tactic:
apply Finset.sum_nbij' (fun m ↦ ⟨m, S m⟩) Prod.fst <;> simp

Goal state after:
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
⊢ Submodule.restrictScalars R (map includeLeft I) = (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range

Tactic:
rw [← SetLike.coe_set_eq]
  apply le_antisymm
  · intro x hx
    simp only [SetLike.mem_coe, LinearMap.mem_range]
    rw [Ideal.map, ← submodule_span_eq] at hx
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
    · intro x
      simp only [includeLeft_apply, Set.mem_image, SetLike.mem_coe]
      rintro ⟨y, hy, rfl⟩
      use ⟨y, hy⟩ ⊗ₜ[R] 1
      rfl
    · use 0
      simp only [map_zero]
    · rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]
    · rintro a x - ⟨x, hx, rfl⟩
      induction a with
      | zero =>
        use 0
        simp only [map_zero, smul_eq_mul, zero_mul]
      | tmul a b =>
        induction x with
        | zero =>
          use 0
          simp only [map_zero, smul_eq_mul, mul_zero]
        | tmul x y =>
          use (a • x) ⊗ₜ[R] (b * y)
          simp only [smul_eq_mul]
          with_unfolding_all rfl
        | add x y hx hy =>
          obtain ⟨x', hx'⟩ := hx
          obtain ⟨y', hy'⟩ := hy
          use x' + y'
          simp only [map_add, hx', smul_add, hy']
      | add a b ha hb =>
        obtain ⟨x', ha'⟩ := ha
        obtain ⟨y', hb'⟩ := hb
        use x' + y'
        simp only [map_add, ha', add_smul, hb']
  · rintro x ⟨y, rfl⟩
    induction y with
    | zero =>
        rw [map_zero]
        apply zero_mem
    | tmul a b =>
        simp only [LinearMap.rTensor_tmul, Submodule.coe_subtype]
        suffices (a : A) ⊗ₜ[R] b = ((1 : A) ⊗ₜ[R] b) * ((a : A) ⊗ₜ[R] (1 : B)) by
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          rw [this]
          apply Ideal.mul_mem_left
          -- Note: adding `includeLeft` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeLeft
          exact Submodule.coe_mem a
        simp only [Algebra.TensorProduct.tmul_mul_tmul,
          mul_one, one_mul]
    | add x y hx hy =>
        rw [map_add]
        apply Submodule.add_mem _ hx hy

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
r u : R
hu : IsUnit u
h_comm : Commute r u
n : ℕ
⊢ r ^ n * u ^ n = 0 ↔ r ^ n = 0

Tactic:
(hu.pow n).mul_left_eq_zero

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
r u : R
hu : IsUnit u
h_comm : Commute r u
n : ℕ
⊢ r ^ n = 0 ↔ r ^ n = 0
Module: Mathlib.Algebra.BigOperators.Field

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype β
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens

Tactic:
simp only [dens, ← sum_div]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype β
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ ↑(#(s.biUnion t)) / ↑(Fintype.card β) ≤ (∑ i ∈ s, ↑(#(t i))) / ↑(Fintype.card β)
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
convert! this (j : Fin (k + 1)) (by grind) using 3 <;> grind [cast_val_eq_self]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
k : ℕ
| f k • g k

Tactic:
← sum_range_succ_sub_sum g

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
k : ℕ
| f k • (∑ i ∈ range (k + 1), g i - ∑ i ∈ range k, g i)
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
⊢ Nat.card ↑(f ⁻¹' ↑s) = ∑ b ∈ s, Nat.card { a // f a = b }

Tactic:
let t := (Set.finite_coe_iff.mp (Finite.Set.finite_inter_of_left ↑s (Set.range f))).toFinset
  rw [show Nat.card (f ⁻¹' s) = Nat.card (f ⁻¹' t) by simp [t]]
  rw [show ∑ b ∈ s, Nat.card {a //f a = b} = ∑ b ∈ t, Nat.card {a | f a = b} by
    exact (Finset.sum_subset (by simp [t]) (by aesop)).symm]
  have ht : Set.Finite (f ⁻¹' t) := Set.Finite.preimage' (finite_toSet t) (by aesop)
  rw [Nat.card_eq_card_finite_toFinset ht, Finset.card_eq_sum_card_image (f := f)]
  refine Finset.sum_congr ?_ fun m hm ↦ ?_
  · simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range
  · rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : Multiset α
xs : List α
⊢ (map f ⟦xs⟧).sym2 = map (Sym2.map f) (Multiset.sym2 ⟦xs⟧)

Tactic:
by simp [List.sym2_map]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ ∅, f i = ⊤ ↔ ∃ i ∈ ∅, f i = ⊤

case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊤ ↔ ∃ i ∈ s✝, f i = ⊤
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊤ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊤
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ ∅, f i = ⊥ ↔ ∃ i ∈ ∅, f i = ⊥

case cons
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∑ i ∈ s✝, f i = ⊥ ↔ ∃ i ∈ s✝, f i = ⊥
⊢ ∑ i ∈ cons a✝¹ s✝ h✝, f i = ⊥ ↔ ∃ i ∈ cons a✝¹ s✝ h✝, f i = ⊥
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ uncurry Sym2.mk '' (f '' s) ×ˢ (f '' s) = Sym2.map f '' uncurry Sym2.mk '' s ×ˢ s

Tactic:
prod_image_image_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ uncurry Sym2.mk '' (fun p ↦ (f p.1, f p.2)) '' s ×ˢ s = Sym2.map f '' uncurry Sym2.mk '' s ×ˢ s
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ inv f ≫ f ≫ g = h

Tactic:
w,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsIso f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ inv f ≫ f ≫ h = h
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g

Tactic:
exact of_isIso_comp_left f g

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Category

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)

Tactic:
rw [IsIso.inv_comp_eq, ← Category.assoc, IsIso.eq_comp_inv]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
by simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
by simp [w]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
by simp [w]

Goal state after: