Theorem: ExtrDisc.extensivity_explicit (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)
⊢ IsIso
    (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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso
    (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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso
    (finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
refine' isIso_of_bijective ⟨extensivity_injective f HIso hOpen, fun y => _⟩
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ∃ a,
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
            ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
        a =
      y

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ∃ a,
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
            ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
        a =
      y
Tactic:
refine' ⟨⟨(inv β (f y)).1, ⟨y, (inv β (f y)).2, _⟩⟩, rfl⟩
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Tactic:
have inj : Function.Injective (inv β) := by intros r s hrs
  convert congr_arg β hrs <;> change _ = (inv β ≫ β) _<;> simp only [IsIso.inv_hom_id]<;> rfl
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Tactic:
apply inj
State after:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd) =
    ↑(CategoryTheory.inv β) (↑f y)

State before:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Tactic:
intro a
State after:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
a : α
⊢ π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a

State before:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
a : α
⊢ π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Tactic:
simp only [IsIso.comp_inv_eq, finiteCoproduct.ι_desc]
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ Function.Injective ↑(CategoryTheory.inv β)
Tactic:
intros r s hrs
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
r s : CoeSort.coe X
hrs : ↑(CategoryTheory.inv β) r = ↑(CategoryTheory.inv β) s
⊢ r = s

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
r s : CoeSort.coe X
hrs : ↑(CategoryTheory.inv β) r = ↑(CategoryTheory.inv β) s
⊢ r = s
Tactic:
convert congr_arg β hrs <;> change _ = (inv β ≫ β) _<;> simp only [IsIso.inv_hom_id]<;> 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd) =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
change (_ ≫ inv β) _ = _
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
rw [this]
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)

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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
rfl
State after:
no goals