-- Mathlib/AlgebraicGeometry/Limits.lean
lemma sigmaι_eq_iff (i j : ι) (x y) :
    (Sigma.ι f i).base x = (Sigma.ι f j).base y ↔
      (Sigma.mk i x : Σ i, f i) = Sigma.mk j y

Proof state:
case pos
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : i = j
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
subst h

Result:
case pos
ι : Type u
f : ι → Scheme
i : ι
x y : ↑↑(f i).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' y
⊢ ⟨i, x⟩ = ⟨i, y⟩

Proof state:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
by_cases h : i = j

Result:
case pos
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : i = j
⊢ ⟨i, x⟩ = ⟨j, y⟩

case neg
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
⊢ ⟨i, x⟩ = ⟨j, y⟩

Proof state:
case neg
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
obtain ⟨z, _⟩ := (Scheme.GlueData.ι_eq_iff _ _ _ _ _).mp H

Result:
case neg.intro
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
z : ↑↑((disjointGlueData f).V (⟨i, x⟩.fst, ⟨j, y⟩.fst)).toPresheafedSpace
h✝ :
  (ConcreteCategory.hom ((disjointGlueData f).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) z = ⟨i, x⟩.snd ∧
    (ConcreteCategory.hom
          ((disjointGlueData f).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (disjointGlueData f).f ⟨j, y⟩.fst ⟨i, x⟩.fst).base)
        z =
      ⟨j, y⟩.snd
⊢ ⟨i, x⟩ = ⟨j, y⟩

Proof state:
case neg.intro
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
z : ↑↑((disjointGlueData f).V (⟨i, x⟩.fst, ⟨j, y⟩.fst)).toPresheafedSpace
h✝ :
  (ConcreteCategory.hom ((disjointGlueData f).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) z = ⟨i, x⟩.snd ∧
    (ConcreteCategory.hom
          ((disjointGlueData f).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (disjointGlueData f).f ⟨j, y⟩.fst ⟨i, x⟩.fst).base)
        z =
      ⟨j, y⟩.snd
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
simp only [disjointGlueData_J, disjointGlueData_V, h, ↓reduceIte] at z

Result:
case neg.intro
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
z✝ : ↑↑((disjointGlueData f).V (⟨i, x⟩.fst, ⟨j, y⟩.fst)).toPresheafedSpace
h✝ :
  (ConcreteCategory.hom ((disjointGlueData f).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) z✝ = ⟨i, x⟩.snd ∧
    (ConcreteCategory.hom
          ((disjointGlueData f).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (disjointGlueData f).f ⟨j, y⟩.fst ⟨i, x⟩.fst).base)
        z✝ =
      ⟨j, y⟩.snd
z : ↑↑∅.toPresheafedSpace
⊢ ⟨i, x⟩ = ⟨j, y⟩

Proof state:
case pos
ι : Type u
f : ι → Scheme
i : ι
x y : ↑↑(f i).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' y
⊢ ⟨i, x⟩ = ⟨i, y⟩

Tactic:
simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]

Result:
case pos
ι : Type u
f : ι → Scheme
i : ι
x y : ↑↑(f i).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' y
⊢ x = y

Proof state:
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y ↔ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
constructor

Result:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y → ⟨i, x⟩ = ⟨j, y⟩

case mpr
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
⊢ ⟨i, x⟩ = ⟨j, y⟩ → (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y

Proof state:
case pos
ι : Type u
f : ι → Scheme
i : ι
x y : ↑↑(f i).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' y
⊢ x = y

Tactic:
exact ((disjointGlueData f).ι i).isOpenEmbedding.injective H

Result:
no goals

Proof state:
case mpr.refl
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f i).base) x

Tactic:
rfl

Result:
no goals

Proof state:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (ConcreteCategory.hom ((disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv).base) x =
    (ConcreteCategory.hom ((disjointGlueData f).ι j ≫ (sigmaIsoGlued f).inv).base) y
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
erw [(TopCat.homeoOfIso
  (Scheme.forgetToTop.mapIso (sigmaIsoGlued f))).symm.injective.eq_iff] at H

Result:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
⊢ ⟨i, x⟩ = ⟨j, y⟩

Proof state:
case neg.intro
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι i))).base.hom' x =
    (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom ((disjointGlueData f).ι j))).base.hom' y
h : ¬i = j
z✝ : ↑↑((disjointGlueData f).V (⟨i, x⟩.fst, ⟨j, y⟩.fst)).toPresheafedSpace
h✝ :
  (ConcreteCategory.hom ((disjointGlueData f).f ⟨i, x⟩.fst ⟨j, y⟩.fst).base) z✝ = ⟨i, x⟩.snd ∧
    (ConcreteCategory.hom
          ((disjointGlueData f).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (disjointGlueData f).f ⟨j, y⟩.fst ⟨i, x⟩.fst).base)
        z✝ =
      ⟨j, y⟩.snd
z : ↑↑∅.toPresheafedSpace
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
cases z

Result:
no goals