-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.Pullback.carrierEquiv`. -/
lemma carrierEquiv_eq_iff {T₁ T₂ : Σ T : Triplet f g, Spec T.tensor} :
    T₁ = T₂ ↔ ∃ e : T₁.1 = T₂.1, (Spec.map (Triplet.tensorCongr e).inv).base T₁.2 = T₂.2

Proof state:
case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ T₁ = T₂ → ∃ (e : T₁.fst = T₂.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd

Tactic:
rintro rfl

Result:
case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ∃ (e : T₁.fst = T₁.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₁.snd

Proof state:
case mpr.mk.mk.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ snd✝ : ↑↑(Spec T.tensor).toPresheafedSpace
e : (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr ⋯).inv).base) ⟨T, snd✝¹⟩.snd = ⟨T, snd✝⟩.snd
⊢ ⟨T, snd✝¹⟩ = ⟨T, snd✝⟩

Tactic:
simpa [e]

Result:
no goals

Proof state:
case mpr.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
T : Triplet f g
snd✝ : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (∃ (e : ⟨T, snd✝⟩.fst = T₂.fst),
      (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) ⟨T, snd✝⟩.snd = T₂.snd) →
    ⟨T, snd✝⟩ = T₂

Tactic:
obtain ⟨T', _⟩ := T₂

Result:
case mpr.mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ : ↑↑(Spec T.tensor).toPresheafedSpace
T' : Triplet f g
snd✝ : ↑↑(Spec T'.tensor).toPresheafedSpace
⊢ (∃ (e : ⟨T, snd✝¹⟩.fst = ⟨T', snd✝⟩.fst),
      (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) ⟨T, snd✝¹⟩.snd = ⟨T', snd✝⟩.snd) →
    ⟨T, snd✝¹⟩ = ⟨T', snd✝⟩

Proof state:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (∃ (e : T₁.fst = T₂.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd) →
    T₁ = T₂

Tactic:
obtain ⟨T, _⟩ := T₁

Result:
case mpr.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
T : Triplet f g
snd✝ : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (∃ (e : ⟨T, snd✝⟩.fst = T₂.fst),
      (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) ⟨T, snd✝⟩.snd = T₂.snd) →
    ⟨T, snd✝⟩ = T₂

Proof state:
case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ ∃ (e : T₁.fst = T₁.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₁.snd

Tactic:
simp

Result:
no goals

Proof state:
case mpr.mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ : ↑↑(Spec T.tensor).toPresheafedSpace
T' : Triplet f g
snd✝ : ↑↑(Spec T'.tensor).toPresheafedSpace
⊢ (∃ (e : ⟨T, snd✝¹⟩.fst = ⟨T', snd✝⟩.fst),
      (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) ⟨T, snd✝¹⟩.snd = ⟨T', snd✝⟩.snd) →
    ⟨T, snd✝¹⟩ = ⟨T', snd✝⟩

Tactic:
rintro ⟨rfl : T = T', e⟩

Result:
case mpr.mk.mk.intro
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ snd✝ : ↑↑(Spec T.tensor).toPresheafedSpace
e : (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr ⋯).inv).base) ⟨T, snd✝¹⟩.snd = ⟨T, snd✝⟩.snd
⊢ ⟨T, snd✝¹⟩ = ⟨T, snd✝⟩

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ T₁ = T₂ ↔ ∃ (e : T₁.fst = T₂.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd

Tactic:
constructor

Result:
case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ T₁ = T₂ → ∃ (e : T₁.fst = T₂.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd

case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (∃ (e : T₁.fst = T₂.fst), (ConcreteCategory.hom (Spec.map (Triplet.tensorCongr e).inv).base) T₁.snd = T₂.snd) →
    T₁ = T₂