awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI_1 :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)
⊢ False

Tactic:
one_ne_zero hI

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI_1 :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)
⊢ False

Tactic:
exact one_ne_zero hI

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI_1 :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
hI :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl) (1 : Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ I.asIdeal = J

Tactic:
have : I.1 = J := congr_arg (·.1) eq
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI_1 :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
hI :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl) (1 : Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
eq : I = { asIdeal := J, isPrime := ⋯ }
this : I.asIdeal = J
⊢ False

Tactic:
h (this ▸ max)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI_1 :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
hI :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl) (1 : Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
eq : I = { asIdeal := J, isPrime := ⋯ }
this : I.asIdeal = J
⊢ False

Tactic:
exact h (this ▸ max)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
⊢ ∀ (y : ↥J.primeCompl),
    IsUnit (M := Localization (M := R) I.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl)
          (↑y : R) :
        Localization (M := R) I.asIdeal.primeCompl)

Tactic:
fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩

Premises used: _private.0.PrimeSpectrum.isMaximal_of_toPiLocalization_surjective.match_2, Algebra.algebraMap, IsUnit, Localization, Subtype.mk, IsLocalization.map_units, Ideal.primeCompl, Subtype.val, DFunLike.coe, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
J : Ideal R
max : J.IsMaximal
le : I.asIdeal ≤ J
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ } 1 :
      (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)
h : ¬I.asIdeal.IsMaximal
hJ :
  Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
          (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
        r :
      Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
    (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
hI :
  Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
      Localization (M := R) I.asIdeal.primeCompl)
    (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
        { asIdeal := J, isPrime := ⋯ }
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
      Localization (M := R) I.asIdeal.primeCompl)
⊢ ∀ (y : ↥J.primeCompl),
    IsUnit (M := Localization (M := R) I.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl)
          (↑y : R) :
        Localization (M := R) I.asIdeal.primeCompl)

Tactic:
exact fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
a :
  ∀ (r : R) (I : PrimeSpectrum S),
    Eq.{u_2 + 1} (α := Localization (M := S) I.asIdeal.primeCompl)
      ((((mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
              RingHom.{u_1, u_2} R (PiLocalization S)) :
            (a : R) → PiLocalization S)
          r I :
        Localization (M := S) I.asIdeal.primeCompl)
      ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
        Localization (M := S) I.asIdeal.primeCompl)
⊢ (mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) =
    RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f

Tactic:
ext r I
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
a :
  Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
          (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
        ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
            (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
          r) :
      Localization.AtPrime I.asIdeal)
    ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
      Localization.AtPrime I.asIdeal)
⊢ Eq.{u_2 + 1} (α := Localization (M := S) I.asIdeal.primeCompl)
    ((((mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization (M := S) I.asIdeal.primeCompl)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization (M := S) I.asIdeal.primeCompl)

Tactic:
change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)

Premises used: Algebra.algebraMap, Localization.localRingHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
a :
  Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
      (Subtype.mk (p := fun (x : S) ↦ x ∈ I.asIdeal.primeCompl) 1 ⋯ : ↥I.asIdeal.primeCompl))
    (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
      (1 : ↥I.asIdeal.primeCompl))
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
          (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
        ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
            (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
          r) :
      Localization.AtPrime I.asIdeal)
    ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
      Localization.AtPrime I.asIdeal)

Tactic:
simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
    ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]

Premises used: Localization.localRingHom_mk', Submonoid.coe_one, map_one, IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
      (Subtype.mk (p := fun (x : S) ↦ x ∈ I.asIdeal.primeCompl) 1 ⋯ : ↥I.asIdeal.primeCompl))
    (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
      (1 : ↥I.asIdeal.primeCompl))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
a :
  ∀ (x : PiLocalization R) (x_1 : PrimeSpectrum R),
    Eq (α := Localization (M := R) x_1.asIdeal.primeCompl)
      ((mapPiLocalization (RingHom.id R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
        Localization (M := R) x_1.asIdeal.primeCompl)
      ((RingHom.id (PiLocalization R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
        Localization (M := R) x_1.asIdeal.primeCompl)
⊢ Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R)) (RingHom.id (PiLocalization R))

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
x : PiLocalization R
x_1 : PrimeSpectrum R
⊢ Eq (α := Localization (M := R) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (RingHom.id R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)
    ((RingHom.id (PiLocalization R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)

Tactic:
congr($(Localization.localRingHom_id _) _)

Premises used: congrArg, Localization.localRingHom_id, id, Localization, Pi.evalRingHom, Ideal.primeCompl, PrimeSpectrum.comap, RingHom.id, DFunLike.coe, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
x : PiLocalization R
x_1 : PrimeSpectrum R
⊢ Eq (α := Localization (M := R) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (RingHom.id R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)
    ((RingHom.id (PiLocalization R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)

Tactic:
exact congr($(Localization.localRingHom_id _) _)
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
f : R →+* S
g : S →+* P
a :
  ∀ (x : PiLocalization R) (x_1 : PrimeSpectrum P),
    Eq.{u_3 + 1} (α := Localization (M := P) x_1.asIdeal.primeCompl)
      ((mapPiLocalization (g.comp f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
        Localization (M := P) x_1.asIdeal.primeCompl)
      (((mapPiLocalization g).comp (mapPiLocalization f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
        Localization (M := P) x_1.asIdeal.primeCompl)
⊢ mapPiLocalization (g.comp f) = (mapPiLocalization g).comp (mapPiLocalization f)

Tactic:
ext
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
f : R →+* S
g : S →+* P
x : PiLocalization R
x_1 : PrimeSpectrum P
⊢ Eq.{u_3 + 1} (α := Localization (M := P) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (g.comp f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)
    (((mapPiLocalization g).comp (mapPiLocalization f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)

Tactic:
congr($(Localization.localRingHom_comp _ _ _ _ rfl _ rfl) _)

Premises used: congrArg, id, Localization, RingHom.comp, Pi.evalRingHom, Ideal.comap, Ideal.primeCompl, Localization.localRingHom_comp, PrimeSpectrum.comap, DFunLike.coe, PrimeSpectrum.asIdeal, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
f : R →+* S
g : S →+* P
x : PiLocalization R
x_1 : PrimeSpectrum P
⊢ Eq.{u_3 + 1} (α := Localization (M := P) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (g.comp f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)
    (((mapPiLocalization g).comp (mapPiLocalization f) : (a : PiLocalization R) → PiLocalization P) x x_1 :
      Localization (M := P) x_1.asIdeal.primeCompl)

Tactic:
exact congr($(Localization.localRingHom_comp _ _ _ _ rfl _ rfl) _)
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (RingHom.comp (β := PiLocalization R) (mapPiLocalization (↑f : R →+* S)) (mapPiLocalization (↑f.symm : S →+* R)))
    (RingHom.id (PiLocalization S))
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R)
    (RingHom.comp (β := PiLocalization S) (mapPiLocalization (↑f.symm : S →+* R)) (mapPiLocalization (↑f : R →+* S)))
    (RingHom.id (PiLocalization R))
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1) : (a : PiLocalization R) → PiLocalization S)

Tactic:
let e := RingEquiv.ofRingHom (mapPiLocalization (f : R →+* S)) (mapPiLocalization f.symm) ?_ ?_