mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ ((isoEqualizer I).hom ≫ equalizer.ι I.fstPiMap I.sndPiMap) ≫ Pi.π I.left a = ι I a

Tactic:
Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝² : HasMultiequalizer I
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
a : J.L
⊢ (isoEqualizer I).hom ≫ equalizer.ι I.fstPiMap I.sndPiMap ≫ Pi.π I.left a = ι I a
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a))) ≫ i =
    (I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a))) ≫ j

Tactic:
Category.assoc,

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a)) ≫ i =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ colimit.ι I.multispan (WalkingMultispan.right (J.fst a)) ≫ j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.η.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.η.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ (T.μ.app c.pt ≫ t.lift (newCone D c)) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = (T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c)) ≫ c.π.app j

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
j : J
⊢ T.μ.app c.pt ≫ t.lift (newCone D c) ≫ c.π.app j = T.map (t.lift (newCone D c)) ≫ t.lift (newCone D c) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c)) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c) ≫ c.π.app j =
    s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = (T.map (D.obj j).a ≫ T.map (c.ι.app j)) ≫ lambda c t

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ (D.obj j).a ≫ c.ι.app j = T.map (D.obj j).a ≫ T.map (c.ι.app j) ≫ lambda c t
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = ((D.obj j).a ≫ c.ι.app j) ≫ t.desc (T.forget.mapCocone s)

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map ((T.forget.mapCocone s).ι.app j) ≫ s.pt.a = (D.obj j).a ≫ c.ι.app j ≫ t.desc (T.forget.mapCocone s)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ ((D.obj j).a ≫ T.map (c.ι.app j)) ≫ T.map (t.desc (T.forget.mapCocone s)) = T.forget.map (s.ι.app j) ≫ s.pt.a

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) = T.forget.map (s.ι.app j) ≫ s.pt.a
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ (s.pt.a ≫ T.map (t.lift (T.forget.mapCone s))) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (c.π.app j)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (t.lift c ≫ c.π.app j) =
    (t.lift (T.forget.mapCone s) ≫ lambda c t) ≫ T.map (t.lift c ≫ c.π.app j)

Tactic:
Category.assoc,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (t.lift c ≫ c.π.app j) =
    t.lift (T.forget.mapCone s) ≫ lambda c t ≫ T.map (t.lift c ≫ c.π.app j)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)

Tactic:
by rw [sSup_eq_iSup', localized₀_iSup, sSup_image']

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
⊢ J ∈ {I.radical}

Tactic:
have le := H.out.isPrime.radical_le_iff.mpr H.le

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
le : I.radical ≤ J
⊢ J ∈ {I.radical}
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ → I = ⊤

pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → I.minimalPrimes = ∅

Tactic:
· intro e
    by_contra h
    have ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h
    have ⟨p, hp⟩ := Ideal.exists_minimalPrimes_le hM'
    rw [e] at hp
    apply Set.notMem_empty _ hp.1

Goal state after:
case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I = ⊤ → I.minimalPrimes = ∅
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
revert x

Goal state after:
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ {x : R}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
⊢ (algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I

Tactic:
rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂

Tactic:
· exact fun hJ => Ideal.comap_mono hJ

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
h : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
⊢ mk' S (a * b) (s * t) ∈ J

Tactic:
rwa [mk'_mul, ha, hb]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if k ∈ (p₁ * p₂).support then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k

Tactic:
mem_support_iff,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if (p₁ * p₂).coeff k ≠ 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
| ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
        ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
    k

Tactic:
coeff_mul

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
| ∑ x ∈ Finset.antidiagonal k,
    (∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))).coeff x.1 *
      (∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff x.2
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if x.1 ∈ p₁.support then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if x.2 ∈ p₂.support then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0

Tactic:
mem_support_iff,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if p₁.coeff x.1 ≠ 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if p₂.coeff x.2 ≠ 0 then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (toFunLinear R A) (1 ⊗ₜ[R] 1) = 1

Tactic:
by
  rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (algebraMap R S) m ∈ I
⊢ 1 = (algebraMap R S) m * mk' S 1 ⟨m, hm⟩

Tactic:
rw [← mk'_eq_mul_mk'_one, mk'_self]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
x✝¹ : R[X]
x✝ : A[X]
n✝ : ℕ
⊢ ∑ p ∈ Finset.antidiagonal n✝, ((mapRingHom (algebraMap R A)) x✝¹).coeff p.swap.1 * x✝.coeff p.swap.2 =
    (x✝ * (mapRingHom (algebraMap R A)) x✝¹).coeff n✝

Tactic:
coeff_mul

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
x✝¹ : R[X]
x✝ : A[X]
n✝ : ℕ
⊢ ∑ p ∈ Finset.antidiagonal n✝, ((mapRingHom (algebraMap R A)) x✝¹).coeff p.swap.1 * x✝.coeff p.swap.2 =
    ∑ x ∈ Finset.antidiagonal n✝, x✝.coeff x.1 * ((mapRingHom (algebraMap R A)) x✝¹).coeff x.2
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ ∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1

Tactic:
refine ⟨⟨z * t', z' * t, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ z' * ↑t ∈ localizationLocalizationSubmodule M N

case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ x * (algebraMap R T) ↑(z * ↑t', ⟨z' * ↑t, ?refine_1⟩).2 = (algebraMap R T) (z * ↑t', ⟨z' * ↑t, ?refine_1⟩).1
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H : ∀ (P : Ideal S) [inst : P.IsMaximal], Flat R (Mₚ P)
⊢ Flat R M

Tactic:
by
  simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
  simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
  refine fun _ _ _ N ↦ injective_of_isLocalized_maximal _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _ fun P hP ↦ ?_
  simpa [IsLocalizedModule.map_lTensor] using H P N

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (sx * sy) • (x + y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
rw [smul_add, mul_smul, mul_smul, Algebra.smul_def sx (sy • y), smul_comm,
      Algebra.smul_def sy (sx • x)]

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Subalgebra R S
hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ
τ : Set T
t : T
ht : t ∈ adjoin S τ
x y : T
sx : S
hsx : sx ∈ σ
hsx' : IsUnit sx
hsx'' : sx • x ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
sy : S
hsy : sy ∈ σ
hsy' : IsUnit sy
hsy'' : sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
⊢ (algebraMap S T) sy * sx • x + (algebraMap S T) sx * sy • y ∈
    Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
P : Type u_3
inst✝³ : CommSemiring P
I✝ : Ideal R
hI : I✝.IsPrime
inst✝² : Algebra R P
I : Ideal S
inst✝¹ : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : S →ₐ[R] P
hIJ : I = Ideal.comap f J
r : R
⊢ (↑↑(localRingHom I J f.toRingHom hIJ)).toFun ((algebraMap R (Localization.AtPrime I)) r) =
    (algebraMap R (Localization.AtPrime J)) r

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime I),
      localRingHom_to_map, IsScalarTower.algebraMap_apply R P (Localization.AtPrime J)]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ x * t₂ • t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆

Goal state after:
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ x = mk' S 1 z • (algebraMap R S) y

Tactic:
rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

Goal state after: