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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
⊢ IsAlgebraic (↥Rt) a

Tactic:
let _ : Algebra Rs Rts := (Subalgebra.inclusion
    (T := Rts.restrictScalars R) <| adjoin_le <| by apply subset_adjoin).toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
Rts : Subalgebra (↥Rt) S := adjoin (↥Rt) s
x✝ : Algebra ↥Rs ↥Rts := (Subalgebra.inclusion ⋯).toAlgebra
⊢ IsAlgebraic (↥Rt) a
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 ↔ m = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ 1 ⊗ₜ[R] m = 0 → m = 0

case mpr
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
⊢ m = 0 → 1 ⊗ₜ[R] m = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case right
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ {{ asIdeal := p_id, isPrime := h_pp }.asIdeal}.prod ≠ ⊥

Tactic:
Multiset.prod_singleton

Goal state after:
case right
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
hA_nont : Nontrivial A
hgt : ∀ J > ⊤, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : ⊤ ≠ ⊥
p_id : Ideal A
h_nzp : p_id ≠ ⊥
h_pp : p_id.IsPrime
⊢ { asIdeal := p_id, isPrime := h_pp }.asIdeal ≠ ⊥
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : M.IsPrime
⊢ {{ asIdeal := M, isPrime := h_prM }.asIdeal}.prod ≤ M ∧ {{ asIdeal := M, isPrime := h_prM }.asIdeal}.prod ≠ ⊥

Tactic:
Multiset.prod_singleton

Goal state after:
case h
A : Type u
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt : ∀ J > M, J ≠ ⊥ → ∃ Z, (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : M.IsPrime
⊢ { asIdeal := M, isPrime := h_prM }.asIdeal ≤ M ∧ { asIdeal := M, isPrime := h_prM }.asIdeal ≠ ⊥
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (M ⊗[R] N)
⊢ LinearMap.lTensor M LinearMap.id = 0

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (M ⊗[R] N)
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝
Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsLocalRing R
inst✝⁴ : CommRing S
inst✝³ : IsLocalRing S
inst✝² : CommRing T
inst✝¹ : IsLocalRing T
f : R →+* S
inst✝ : IsLocalHom f
a : R
ha : a ∈ maximalIdeal R
⊢ ((Ideal.Quotient.mk (maximalIdeal S)).comp f) a = 0

Tactic:
unfold ResidueField
    rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem]
    exact map_nonunit f a ha

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝³ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝² : AddCommGroup N
x✝¹ : Module R N
x✝ : Subsingleton (N ⊗[R] M)
⊢ LinearMap.rTensor M LinearMap.id = 0

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (N ⊗[R] M)
x✝¹ : N
x✝ : M
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) ↔
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) →
    ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x

case mpr
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
P : Ideal S
inst✝ : P.IsPrime
⊢ (∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) →
    Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
⊢ Algebra.IsAlgebraic K L

Tactic:
constructor

Goal state after:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field K
inst✝⁹ : CommRing L
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : IsFractionRing S L
inst✝ : Algebra.IsIntegral R S
⊢ ∀ (x : L), IsAlgebraic K x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * 0 = a ⊗ₜ[R] t

Tactic:
exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩

Goal state after:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
⊢ LinearMap.lTensor S (LinearMap.lTensor M f) =
    ↑(TensorProduct.assoc R S M P) ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ ↑(TensorProduct.assoc R S M N).symm

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : FaithfullyFlat R S
inst✝⁴ : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
hf : Function.Injective ⇑f
this : Flat R (S ⊗[R] M)
x✝² : S
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (LinearMap.lTensor S (LinearMap.lTensor M f))) x✝²)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              (↑(TensorProduct.assoc R S M P) ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ ↑(TensorProduct.assoc R S M N).symm))
            x✝²))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R T')).comp
      ((↑(Algebra.TensorProduct.comm R T' S)).comp
        ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))

Tactic:
ext

Goal state after:
case ha
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : S
⊢ ((Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
            ((↑(Algebra.TensorProduct.comm R T' S)).comp
              ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T)))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

case hb
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
T : Type u_3
inst✝⁶ : CommRing T
S' : Type u_4
T' : Type u_5
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map f g)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map f (AlgHom.id R T')).comp
              ((↑(Algebra.TensorProduct.comm R T' S)).comp
                ((Algebra.TensorProduct.map g (AlgHom.id R S)).comp ↑(Algebra.TensorProduct.comm R S T))))).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
⊢ FaithfulSMul A B

Tactic:
constructor

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : FaithfullyFlat A B
⊢ ∀ {m₁ m₂ : A}, (∀ (a : B), m₁ • a = m₂ • a) → m₁ = m₂
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
inst✝ : I.IsPrime
⊢ mapₐ I I (AlgHom.id R A) ⋯ = AlgHom.id R I.ResidueField

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
inst✝ : I.IsPrime
x✝ : A
⊢ ((mapₐ I I (AlgHom.id R A) ⋯).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝ =
    ((AlgHom.id R I.ResidueField).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i, I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i, I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical

case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i, I.IsMinimalPrime i ∧ x ∈ i
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑b * ↑b) = ↑a * ↑b

Tactic:
rw [b.2]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
⊢ {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} = ↑(mapToFractionRing K S (Localization S) hS).range

Tactic:
ext

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS✝ : S ≤ A⁰
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
hS : S ≤ A⁰
x✝ : K
⊢ x✝ ∈ {x | ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩} ↔
    x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹} =
    ↑(mapToFractionRing K S (Localization S) hS).range

Tactic:
ext

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹} ↔
    x✝ ∈ ↑(mapToFractionRing K S (Localization S) hS).range
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes ↔ J ∈ comap f '' I.minimalPrimes

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes ↔ p ∈ Ideal.under R ⁻¹' J.minimalPrimes

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes → p ∈ Ideal.under R ⁻¹' J.minimalPrimes

case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.under R (IsLocalRing.maximalIdeal A) ∈ I.minimalPrimes

Tactic:
under_maximalIdeal A q

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ q ∈ I.minimalPrimes
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

case mpr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ (∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mp
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂

Goal state after:
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case mpr
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i) ∧ IsOpen (⋃ i ∈ s, b i)

Tactic:
constructor

Goal state after:
case mpr.left
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact (⋃ i ∈ s, b i)

case mpr.right
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen (⋃ i ∈ s, b i)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔
    x ∈ range ⇑(algebraMap R K)

Tactic:
constructor

Goal state after:
case mp
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) →
    x ∈ range ⇑(algebraMap R K)

case mpr
R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ range ⇑(algebraMap R K) → ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (toPiLocalization (R i)) (r i) I = (toPiLocalization (R i)) (0 i) I

Tactic:
toPiLocalization_apply_apply,

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (algebraMap (R i) (Localization.AtPrime I.asIdeal)) (r i) = (algebraMap (R i) (Localization.AtPrime I.asIdeal)) (0 i)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ mapPiLocalization (RingHom.id R) = RingHom.id (PiLocalization R)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝¹ : PiLocalization R
x✝ : PrimeSpectrum R
⊢ (mapPiLocalization (RingHom.id R)) x✝¹ x✝ = (RingHom.id (PiLocalization R)) x✝¹ x✝
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ mapPiLocalization (RingHom.id R) = RingHom.id (PiLocalization R)

Tactic:
by
  ext; exact congr($(Localization.localRingHom_id _) _)

Goal state after: