mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ 0 * 1 ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
⊢ ∀ (c : B) (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x y : B ⧸ Ideal.map (algebraMap A B) I
⊢ (quotIdealMapEquivTensorQuotAux B I) (x * y) =
    (quotIdealMapEquivTensorQuotAux B I) x * (quotIdealMapEquivTensorQuotAux B I) y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x : A
this :
  (TensorProduct.comm A B (A ⧸ I))
      ((quotIdealMapEquivTensorQuot B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) ((algebraMap A B) x))) =
    (algebraMap A ((A ⧸ I) ⊗[A] B)) x
⊢ ((quotIdealMapEquivTensorQuot B I).toRingEquiv.trans (TensorProduct.comm A B (A ⧸ I)).toRingEquiv).toFun
      ((algebraMap A (B ⧸ Ideal.map (algebraMap A B) I)) x) =
    (algebraMap A ((A ⧸ I) ⊗[A] B)) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x : A
⊢ ((quotIdealMapEquivTensorQuot B I).toRingEquiv.trans (TensorProduct.comm A B (A ⧸ I)).toRingEquiv).toFun
      ((algebraMap A (B ⧸ Ideal.map (algebraMap A B) I)) x) =
    (algebraMap A ((A ⧸ I) ⊗[A] B)) x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
⊢ 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
by

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

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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
⊢ x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z, x = mk' S 1 z • y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
⊢ ∀ (x y : A ⊗[R] (T ⧸ I)),
    (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (x * y) =
      (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) x *
        (AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ (↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M (Submodule.subtype I)).range = I • ⊤

Tactic:
by

Goal state after:
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✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
⊢ R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0

Tactic:
by

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

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
x : S
a : Set R
⊢ x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ (x + y) * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩

Goal state after:
case h.add
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
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ (x + y) * (tx * ty) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
⊢ (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ OfLocalizationSpan P ↔ OfLocalizationFiniteSpan P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
⊢ Ideal.span {φ e} ≤ RingHom.ker ψ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
⊢ Ideal.map φ (Ideal.span {e}) ≤ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
⊢ (TensorProduct.lift (ofId R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}))
          (Ideal.quotientMapₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) φ ⋯) ⋯).comp
      (Ideal.Quotient.liftₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) ψ heψ) =
    AlgHom.id R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
⊢ (equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)) =
    (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.rTensor S (ofId R' R'')
ψ : R'' ⊗[R] S →ₐ[R''] R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}) :=
  TensorProduct.lift (ofId R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e})))
    ((AlgHom.restrictScalars R TensorProduct.includeRight).comp
      ((Ideal.Quotient.mkₐ R (Ideal.span {e})).comp TensorProduct.includeRight))
    ⋯
hψφ :
  (AlgHom.restrictScalars R' ψ).comp φ =
    (AlgHom.restrictScalars R' TensorProduct.includeRight).comp (Ideal.Quotient.mkₐ R' (Ideal.span {e}))
heψ : Ideal.span {φ e} ≤ RingHom.ker ψ
⊢ (Ideal.Quotient.liftₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) ψ heψ).comp
      (TensorProduct.lift (ofId R'' (R'' ⊗[R] S ⧸ Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}))
        (Ideal.quotientMapₐ (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e}) φ ⋯) ⋯) =
    AlgHom.id R'' (R'' ⊗[R'] (R' ⊗[R] S ⧸ Ideal.span {e}))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
h : EssFiniteType R S
⊢ EssFiniteType T (T ⊗[R] S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
a : R''
b : R'
c : S
⊢ (tensorQuotientTensorEquiv R'' e) (a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (b ⊗ₜ[R] c)) =
    (Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) ((a * (algebraMap R' R'') b) ⊗ₜ[R] c)

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ OfLocalizationSpanTarget P ↔ OfLocalizationFiniteSpanTarget P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
R' : Type u_2
R'' : Type u_3
S : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing R''
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R R''
inst✝² : Algebra R' R''
inst✝¹ : IsScalarTower R R' R''
inst✝ : Algebra R S
e : R' ⊗[R] S
a : R''
b : S
⊢ (tensorQuotientTensorEquiv R'' e).symm
      ((Ideal.Quotient.mk (Ideal.span {(TensorProduct.rTensor S (ofId R' R'')) e})) (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R'] (Ideal.Quotient.mk (Ideal.span {e})) (1 ⊗ₜ[R] b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

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 S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
ι : Type u_4
v : ι → S
⊢ Set.InjOn ⇑(IsScalarTower.toAlgHom R S A).toLinearMap ↑(Submodule.span R (Set.range v))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Algebra

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 S
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : FaithfulSMul S A
s : Set S
⊢ Set.InjOn (⇑(algebraMap S A)) s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
⊢ IsRightRegular k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
k : α
h : IsRegular k
⊢ k ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ x * (1 - y * x + y) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
h : EssFiniteType R T
⊢ EssFiniteType S T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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
f : S →ₐ[R] T
hf : Function.Surjective ⇑f
inst✝ : EssFiniteType R S
⊢ EssFiniteType R T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ (1 - y * x + x) * y = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.toRingHom = g.toRingHom
⊢ f = g

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hf : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ P) (Localization.awayMap f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
x✝ : (r : R) → Algebra (Localization.Away r) (Localization.Away ((algebraMap R S) r)) :=
  fun r ↦ (Localization.awayMap (algebraMap R S) r).toAlgebra
r : R
hr : r ∈ s
⊢ algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
    (↑(IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm).comp
      (algebraMap (Localization.Away r) (Localization.Away ((algebraMap R S) r)))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.comp (IsScalarTower.toAlgHom R ?m.97 S) = g.comp (IsScalarTower.toAlgHom R ?m.97 S)
⊢ f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H : ∀ {R : Type u} [inst : CommRing R] (M : Submonoid R), P (algebraMap R (Localization M))
⊢ HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

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

Goal state before:
pp: R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization fun {R S} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : Algebra R R'
inst✝³ : IsLocalization M R'
S' : Type u
inst✝² : CommRing S'
inst✝¹ : Algebra S S'
inst✝ : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
⊢ Submonoid.map f M ≤ T

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: 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✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).EssFiniteType ↔ Algebra.EssFiniteType R S

Tactic:
by

Goal state after: