mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ G.map A.a ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj ((𝟭 D).obj A.1))

pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj ((𝟭 D).obj A.1))

Tactic:
· rw [← G.map_comp, ← G.map_id]
    exact congr_arg G.map A.counit

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
⊢ adj.unit.app (G.obj A.A) ≫ G.map (adj.counit.app A.1) = 𝟙 (G.obj ((𝟭 D).obj A.1))
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ PreservesFiniteLimits (tensorLeft M)

Tactic:
rw [← iff_preservesFiniteLimits_tensorLeft]

Goal state after:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
⊢ Flat R ↑M
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
R : D ⥤ C
inst✝¹ : ComonadicLeftAdjoint R
inst✝ : PreservesLimitsOfShape J R
⊢ PreservesLimitsOfShape J (comonadicRightAdjoint R)

Tactic:
apply (Adjunction.rightAdjoint_preservesLimits (comonadicAdjunction R)).1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ (Functor.Final.extendCocone.obj
            { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f ↦ F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }).ι.app
      zero =
    G.π

Tactic:
rw [Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f ↦ F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }.ι.app
        WalkingParallelPair.one =
    G.π
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (g * s⁻¹) • x - s⁻¹ • x ∈ s⁻¹ • P

Tactic:
mul_smul,

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ g • s⁻¹ • x - s⁻¹ • x ∈ s⁻¹ • P
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * t) • i ∈ M''

Tactic:
mul_smul,

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ k • t • i ∈ M''
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x

Tactic:
mul_smul,

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ IsLocalizedModule.mk' f (k • t • i) (k * s * t) = x
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I.radical ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ ((algebraMap R S) r * IsLocalization.mk' S 1 s) • n ∈ I • restrictScalars R N'

Tactic:
mul_smul,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ (algebraMap R S) r • IsLocalization.mk' S 1 s • n ∈ I • restrictScalars R N'
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case pos
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit ((mk (I ^ n)) x)

Tactic:
rw [pow_eq_top_iff.mpr (Or.inr hn)]

Goal state after:
case pos
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit ((mk ⊤) x)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
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
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

Tactic:
refine fun h =>
      ⟨⟨?_, ?_⟩,
        Set.disjoint_left.mpr fun m hm1 hm2 =>
          h.ne_top (Ideal.eq_top_of_isUnit_mem _ hm2 (map_units S ⟨m, hm1⟩))⟩

Goal state after:
case mp.refine_1
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 : J.IsPrime
⊢ Ideal.under R J ≠ ⊤

case mp.refine_2
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 : J.IsPrime
⊢ ∀ {x y : R}, x * y ∈ Ideal.under R J → x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r)
⊢ False

Tactic:
let r : s := ⟨r, hrs⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r)
⊢ False

Tactic:
let r : s := ⟨r, hrs⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False
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₁ * p₂).support, if n = k then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff n) 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:
Finset.sum_ite_eq',

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 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
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,
      (∑ x_1 ∈ p₁.support, if x_1 = x.1 then a₁ * (algebraMap R A) (p₁.coeff x_1) else 0) *
        ∑ x_1 ∈ p₂.support, if x_1 = x.2 then a₂ * (algebraMap R A) (p₂.coeff x_1) else 0

Tactic:
Finset.sum_ite_eq',

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 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
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
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 : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
Ideal.Quotient.maximal_ideal_iff_isField_quotient

Goal state after:
case neg
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 : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: 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'
⊢ (algebraMap R S) (z' * ↑t) = ↑s * (algebraMap R S) ↑(t * t')

Tactic:
rw [map_mul, ← eq₃, mul_assoc, ← map_mul, mul_comm t, Submonoid.coe_mul]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
⊢ localized₀ J.primeCompl (g J) G.ker = localized₀ J.primeCompl (g J) F.range

Tactic:
← LinearMap.range_localizedMap_eq_localized₀_range _ (f J) (g J) F,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
⊢ localized₀ J.primeCompl (g J) G.ker = ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
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 + (sx * sy) • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
mul_smul,

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 τ
⊢ sx • sy • x + (sx * sy) • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
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 + (sx * sy) • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ

Tactic:
mul_smul,

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 τ
⊢ sx • sy • x + sx • sy • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ adjoin R τ
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case refine_4
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:
mul_smul,

Goal state after:
case refine_4
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 τ
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M ⊗[R] (N ⧸ n)
⊢ (↑(TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n))).toFun (m • x) =
    (RingHom.id A) m • (↑(TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n))).toFun x

Tactic:
by
    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe]
    induction x with
    | zero => simp
    | add x y hx hy => simp [hx, hy]
    | tmul x y =>
      obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ y
      rw [smul_tmul']
      rfl

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
⊢ (t₁ * t₂) • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
mul_smul,

Goal state after:
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
⊢ t₁ • t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t