-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_bijective : Function.Bijective (mapPiLocalization f hf)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)

Tactic:
simp_rw [RingEquiv.symm_comp, mapPiLocalization_id]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)

Tactic:
simp_rw [RingEquiv.comp_symm, mapPiLocalization_id]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
e : PiLocalization R ≃+* PiLocalization S :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f) hf) (mapPiLocalization ↑f.symm ⋯) ?refine_1 ?refine_2
⊢ Function.Bijective ⇑(mapPiLocalization f✝ hf)

Tactic:
exact e.bijective

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ Function.Bijective ⇑(mapPiLocalization f hf)

Tactic:
let f := RingEquiv.ofBijective f hf

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ Function.Bijective ⇑(mapPiLocalization f✝ hf)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ Function.Bijective ⇑(mapPiLocalization f✝ hf)

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

Result:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
e : PiLocalization R ≃+* PiLocalization S :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f) hf) (mapPiLocalization ↑f.symm ⋯) ?refine_1 ?refine_2
⊢ Function.Bijective ⇑(mapPiLocalization f✝ hf)

case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization (↑f) hf).comp (mapPiLocalization ↑f.symm ⋯) = RingHom.id (PiLocalization S)

case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm ⋯).comp (mapPiLocalization (↑f) hf) = RingHom.id (PiLocalization R)

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization ↑f.symm ⋯).comp (mapPiLocalization (↑f) hf) = RingHom.id (PiLocalization R)

Tactic:
rw [← mapPiLocalization_comp]

Result:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ (mapPiLocalization (↑f) hf).comp (mapPiLocalization ↑f.symm ⋯) = RingHom.id (PiLocalization S)

Tactic:
rw [← mapPiLocalization_comp]

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)