-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[ext]
protected lemma ext {t₁ t₂ : Triplet f g} (ex : t₁.x = t₂.x) (ey : t₁.y = t₂.y) : t₁ = t₂

Proof state:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↑↑X.toPresheafedSpace
y✝¹ : ↑↑Y.toPresheafedSpace
s✝¹ : ↑↑S.toPresheafedSpace
hx✝¹ : (ConcreteCategory.hom f.base) x✝¹ = s✝¹
hy✝¹ : (ConcreteCategory.hom g.base) y✝¹ = s✝¹
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ x✝¹ = x✝ ∧ y✝¹ = y✝ ∧ s✝¹ = s✝

Tactic:
aesop

Result:
no goals

Proof state:
case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂

Tactic:
cases t₂

Result:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↑↑X.toPresheafedSpace
y✝¹ : ↑↑Y.toPresheafedSpace
s✝¹ : ↑↑S.toPresheafedSpace
hx✝¹ : (ConcreteCategory.hom f.base) x✝¹ = s✝¹
hy✝¹ : (ConcreteCategory.hom g.base) y✝¹ = s✝¹
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₁ t₂ : Triplet f g
ex : t₁.x = t₂.x
ey : t₁.y = t₂.y
⊢ t₁ = t₂

Tactic:
cases t₁

Result:
case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂

Proof state:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↑↑X.toPresheafedSpace
y✝¹ : ↑↑Y.toPresheafedSpace
s✝¹ : ↑↑S.toPresheafedSpace
hx✝¹ : (ConcreteCategory.hom f.base) x✝¹ = s✝¹
hy✝¹ : (ConcreteCategory.hom g.base) y✝¹ = s✝¹
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }

Tactic:
simp

Result:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↑↑X.toPresheafedSpace
y✝¹ : ↑↑Y.toPresheafedSpace
s✝¹ : ↑↑S.toPresheafedSpace
hx✝¹ : (ConcreteCategory.hom f.base) x✝¹ = s✝¹
hy✝¹ : (ConcreteCategory.hom g.base) y✝¹ = s✝¹
x✝ : ↑↑X.toPresheafedSpace
y✝ : ↑↑Y.toPresheafedSpace
s✝ : ↑↑S.toPresheafedSpace
hx✝ : (ConcreteCategory.hom f.base) x✝ = s✝
hy✝ : (ConcreteCategory.hom g.base) y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ x✝¹ = x✝ ∧ y✝¹ = y✝ ∧ s✝¹ = s✝