Theorem: ExtrDisc.extensivity_injective (ExtrDisc/ExplicitSheaves.lean)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let ζ := finiteCoproduct.desc _ (fun a => pullback.snd f (hOpen a) ≫ finiteCoproduct.ι Z a )
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let α := finiteCoproduct.desc _ ((fun a => pullback.fst f (hOpen a)))
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let β := finiteCoproduct.desc _ π
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
have comm : ζ ≫ β = α ≫ f := by
   refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
   simp [← Category.assoc, finiteCoproduct.ι_desc, ExtrDisc.pullback.condition]
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
intro R₁ R₂ hR
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ R₁ = R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ R₁ = R₂
Tactic:
have himage : (ζ ≫ β) R₁ = (ζ ≫ β) R₂ := by
  rw [comm]; change f (α R₁) = f (α R₂); rw [hR]
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂
Tactic:
replace himage := congr_arg (inv β) himage
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂
Tactic:
change ((ζ ≫ β ≫ inv β) R₁) = ((ζ ≫ β ≫ inv β) R₂) at himage
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂
Tactic:
rw [IsIso.hom_inv_id, Category.comp_id] at himage
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
⊢ R₁ = R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
⊢ R₁ = R₂
Tactic:
exact Sigma.subtype_ext Hfst hR
State after:
no goals

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ ζ ≫ β = α ≫ f
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
a : α✝
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ ζ ≫ β =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ α ≫ f

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
a : α✝
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ ζ ≫ β =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ α ≫ f
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, ExtrDisc.pullback.condition]
State after:
no goals

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
Tactic:
rw [comm]
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑(α ≫ f) R₁ = ↑(α ≫ f) R₂

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑(α ≫ f) R₁ = ↑(α ≫ f) R₂
Tactic:
change f (α R₁) = f (α R₂)
State after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑f (↑α R₁) = ↑f (↑α R₂)

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑f (↑α R₁) = ↑f (↑α R₂)
Tactic:
rw [hR]
State after:
no goals

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
⊢ (↑ζ R₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
Tactic:
constructor <;> rfl
State after:
no goals

State before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
this : (↑ζ R₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
⊢ R₁.fst = R₂.fst
Tactic:
rw [← this.1, ← this.2, himage]
State after:
no goals