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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
modByMonic,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (if hq : q.Monic then ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux hq).2
    else p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ (have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ∀ x ∈ ⊤, IsAlgebraic R x

Tactic:
simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)

Tactic:
← Polynomial.map_mul,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ (∀ {i : Set (Set α)}, i.Finite ∧ i ⊆ s → (⋂₀ i).Nonempty) ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty

Tactic:
simp only [← and_imp, and_comm]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
f g : Filter α
s : Set α
a : α
⊢ ∀ (b : Set α) (x : α), (∀ (s : Set α), (∀ x ∈ b, x ∈ s) → x ∈ s) → x ∈ b

Tactic:
aesop

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

Goal state before:
pp: α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x

Tactic:
simp [hI]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g → ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s

pp: case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
· rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
    exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g
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⟩ <;> try exact Or.inl ha

Goal state after:
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
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ comap (fun x ↦ ((Equiv.prodAssoc α β γ).symm x).1.1) f ⊓
      (comap (fun x ↦ ((Equiv.prodAssoc α β γ).symm x).1.2) g ⊓ comap (fun x ↦ ((Equiv.prodAssoc α β γ).symm x).2) h) =
    comap Prod.fst f ⊓ (comap (fun x ↦ x.2.1) g ⊓ comap (fun x ↦ x.2.2) h)

Tactic:
Equiv.prodAssoc_symm_apply

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

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ a \ ∂ a = ￢￢a

Tactic:
rw (occs := [1]) [← hnot_hnot_sup_boundary a]
  rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ degree (comapDomain (⇑e) y ⋯) ≤ degree x

pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ ↑y.support ⊆ range ⇑e

Tactic:
· rw [← hy, degree_mapDomain]
    exact degree_comapDomain_le_of_canonicallyOrderedAdd ..

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ ↑y.support ⊆ range ⇑e
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : 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)
⊢ f.support.Nonempty

Tactic:
aesop

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

Goal state before:
pp: α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
⊢ f.support.Nonempty

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ y ~ᵤ p

Tactic:
Associated.comm

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ p ~ᵤ y
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) p * map (algebraMap T S) q ≠ 0

Tactic:
← Polynomial.map_mul,

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) (p * q) ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
· congr 1
    rw [← Multiset.map_eq_map Subtype.coe_injective]
    apply unique' _ _ h <;>
      · intro a ha
        obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha
        rwa [Subtype.coe_mk]

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

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

Tactic:
modByMonic,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (if hq : (q * C q.leadingCoeff⁻¹).Monic then (p.divModByMonicAux hq).2 else p) = p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x * map f (C x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y

Tactic:
← Polynomial.map_mul,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f (x * C x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: K : Type u_1
inst✝ : CommRing K
f : K[X]
a : K
⊢ ?m.57

Tactic:
apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a

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
x : R
⊢ (aeval ((algebraMap R A) x)) (X - C x) = 0

Tactic:
rw [map_sub, aeval_X, aeval_C, sub_self]

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : IsCentral S R
T : End R M
hT : T ∈ Subalgebra.center S (End R M)
w✝ : R
h : w✝ ∈ Subalgebra.center S R
h✝¹ : T = End.smulLeft w✝ h
y : S
h✝ : (ofId S R).toRingHom y = w✝
⊢ (ofId S (End R M)).toRingHom y = T

Tactic:
aesop

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

Tactic:
Algebra.transcendental_iff_not_isAlgebraic

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

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
H : ¬Algebra.IsAlgebraic R A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ¬Algebra.IsAlgebraic S B
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
h : Transcendental R s
f : R[X]
⊢ (algEquivOfTranscendental R s h).symm ((aeval ⟨s, ⋯⟩) f) = f

Tactic:
apply (algEquivOfTranscendental R s h).toEquiv.injective
  simp

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
h : Transcendental R s
⊢ (algEquivOfTranscendental R s h).symm ⟨s, ⋯⟩ = X

Tactic:
apply (algEquivOfTranscendental R s h).toEquiv.injective
  simp

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) 0) =
    (LinearMap.rTensor M (of R ι G f x✝²)) 0

Tactic:
aesop

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x : G x✝²) (y : M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x ⊗ₜ[R] y)) =
      (LinearMap.rTensor M (of R ι G f x✝²)) (x ⊗ₜ[R] y)

Tactic:
aesop

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝² ⊗[R] M
⊢ ∀ (x y : G x✝² ⊗[R] M),
    (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) x) =
        (LinearMap.rTensor M (of R ι G f x✝²)) x →
      (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) y) =
          (LinearMap.rTensor M (of R ι G f x✝²)) y →
        (LinearMap.rTensor M (of R ι G f x✝¹)) ((LinearMap.rTensor M (f x✝² x✝¹ x✝)) (x + y)) =
          (LinearMap.rTensor M (of R ι G f x✝²)) (x + y)

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ι
h : i ≤ j
⊢ ∀ (x : G i),
    ((mk R (G i) M).compr₂ₛₗ (↑(TensorProduct.comm R (G j) M) ∘ₗ LinearMap.rTensor M (f i j h))) x =
      ((mk R (G i) M).compr₂ₛₗ (LinearMap.lTensor M (f i j h) ∘ₗ ↑(TensorProduct.comm R (G i) M))) x

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (piSplitLE
        (fun j ↦ equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨k, hk✝⟩)
      (f h x) l =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨i⁺, hj⟩)
        x)
      l

Tactic:
piSplitLE_lt (lt_succ hk),

Goal state after:
case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ ((fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
        ⟨k, ⋯⟩)
      (f h x) l =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨i⁺, hj⟩)
        x)
      l
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h✝ : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (equiv x✝¹) (f h (↑t x✝)) = piLTProj h ((equiv x✝) (↑t x✝))

Tactic:
apply nat

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
equivLim : F i ≃ ↑(limit f i)
hi : IsSuccPrelimit i
inst✝ : InverseSystem f
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
j k : ι
hj✝ : j ∈ Iic i
hk : k ∈ Iic i
h : k ≤ j
t : F j
hj : j < i
⊢ ((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨k, ⋯⟩) (f h t) =
    piLTProj h (((equiv, equivLim.trans ((invLimEquiv nat).trans (piLTLim hi).symm)).1 ⟨j, hj⟩) t)

Tactic:
apply nat

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : ¬∑ x_1 ∈ Finset.antidiagonal m, coeff x_1.1 x * coeff x_1.2 y = 0
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal m
e : coeff (i, j).1 x * coeff (i, j).2 y ≠ 0
⊢ j ∈ y.support

Tactic:
aesop

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 ⇑(lTensor Q f) ⇑(lTensor Q g)

Tactic:
exact_iff,

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
⊢ (lTensor Q g).ker = (lTensor Q f).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

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

Tactic:
induction a with

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

Goal state before:
pp: 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 B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
a : A ⊗[R] B
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
induction a with

Goal state after:
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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl w✝ N').range
⊢ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range

Tactic:
rw [mapIncl, ← LinearMap.lTensor_comp_rTensor] at h

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
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w✝.subtype).range
⊢ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (x * y)

Tactic:
h_comm.eq

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)

Tactic:
exact h_comm.symm.isNilpotent_mul_right h

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : x ∈ Subalgebra.map includeRight (Subalgebra.center K C)
⊢ x ∈ Subalgebra.center K (B ⊗[K] C)

Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
  obtain ⟨c, hc0, rfl⟩ := hx
  intro bc
  induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

Goal state after: