-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toΓSpecCApp_iff
    (f :
      (structureSheaf <| Γ.obj <| op X).val.obj (op <| basicOpen r) ⟶
        X.presheaf.obj (op <| X.toΓSpecMapBasicOpen r)) :
    toOpen _ (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r

Proof state:
case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))) →
    f = X.toΓSpecCApp r

Tactic:
intro h

Result:
case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))
⊢ f = X.toΓSpecCApp r

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
⊢ toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r

Tactic:
have loc_inst := IsLocalization.to_basicOpen (Γ.obj (op X)) r

Result:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r

Tactic:
refine ConcreteCategory.ext_iff.trans ?_

Result:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) = ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r) ↔
    f = X.toΓSpecCApp r

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) = ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r) ↔
    f = X.toΓSpecCApp r

Tactic:
rw [← @IsLocalization.Away.lift_comp _ _ _ _ _ _ _ r loc_inst _
    (X.isUnit_res_toΓSpecMapBasicOpen r)]

Result:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))) ↔
    f = X.toΓSpecCApp r

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))) ↔
    f = X.toΓSpecCApp r

Tactic:
constructor

Result:
case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))) →
    f = X.toΓSpecCApp r

case mpr
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ f = X.toΓSpecCApp r →
    ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))

Proof state:
case mpr
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
⊢ f = X.toΓSpecCApp r →
    ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))

Tactic:
apply congr_arg

Result:
no goals

Proof state:
case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))
⊢ f = X.toΓSpecCApp r

Tactic:
ext : 1

Result:
case mp.hf
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)

Proof state:
case mp.hf
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r)))
h :
  ConcreteCategory.hom (toOpen (↑(Γ.obj (op X))) (basicOpen r) ≫ f) =
    (IsLocalization.Away.lift r ⋯).comp
      (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).val.obj (op (basicOpen r))))
⊢ CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)

Tactic:
exact IsLocalization.ringHom_ext (Submonoid.powers r) h

Result:
no goals