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

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
have hOpen := openEmbedding_of_sigma_desc_iso H
State after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let θ := Sigma.mapIso (fun a => fromExplicitIso f (hOpen a))
State after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let δ := FromFiniteCoproductIso (fun a => (OpenEmbeddingCone f (hOpen a)).pt)
State after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
convert extensivity_explicit f HIso hOpen
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, fromExplicit]
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
this : IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left θ.hom
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
this : IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
apply IsIso.of_isIso_comp_left δ.hom
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
let ε := ToFiniteCoproductIso Z
State after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
Tactic:
convert H
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
⊢ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.desc i
Tactic:
refine' Sigma.hom_ext _ _ (fun a => _)
State after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i

State before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
a : α
⊢ Sigma.ι Z a ≫ ε.hom ≫ finiteCoproduct.desc Z i = Sigma.ι Z a ≫ Sigma.desc i
Tactic:
simp [← Category.assoc]
State after:
no goals

State before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
ε : ∐ Z ≅ finiteCoproduct Z := ToFiniteCoproductIso Z
this : IsIso (ε.hom ≫ finiteCoproduct.desc Z i)
⊢ IsIso (finiteCoproduct.desc (fun a => Z a) i)
Tactic:
apply IsIso.of_isIso_comp_left ε.hom
State after:
no goals