Theorem: Profinite.extensivity_explicit (Profinite/ExplicitSheaves.lean)

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
⊢ IsIso (finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let β := finiteCoproduct.desc _ π
State after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso (finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso (finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
apply isIso_of_bijective _
State after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Bijective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Bijective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
refine' ⟨extensivity_injective f HIso, fun y => _⟩
State after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) a = y

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
⊢ ∃ a, ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) a = y
Tactic:
refine' ⟨⟨(inv β (f y)).1, ⟨⟨y, (inv β (f y)).2⟩, _⟩⟩, rfl⟩
State after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
⊢ (y, (↑(CategoryTheory.inv β) (↑f y)).snd) ∈ {xy | ↑f xy.fst = ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) xy.snd}

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
⊢ (y, (↑(CategoryTheory.inv β) (↑f y)).snd) ∈ {xy | ↑f xy.fst = ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) xy.snd}
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 : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ (y, (↑(CategoryTheory.inv β) (↑f y)).snd) ∈ {xy | ↑f xy.fst = ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) xy.snd}

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ (y, (↑(CategoryTheory.inv β) (↑f y)).snd) ∈ {xy | ↑f xy.fst = ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) xy.snd}
Tactic:
apply inj
State after:
case a
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst) =
    ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd)

State before:
case a
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Tactic:
intro a
State after:
case a
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
a : α
⊢ π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a

State before:
case a
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj 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 : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
⊢ Function.Injective ↑(CategoryTheory.inv β)
Tactic:
intros r s hrs
State after:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
r s : (forget Profinite).obj X
hrs : ↑(CategoryTheory.inv β) r = ↑(CategoryTheory.inv β) s
⊢ r = s

State before:
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
r s : (forget Profinite).obj 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 : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst) =
    ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd)
Tactic:
apply Eq.symm
State after:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd) =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)

State before:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd) =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)
Tactic:
change (_ ≫ inv β) _ = _
State after:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)

State before:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)
Tactic:
rw [this]
State after:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)

State before:
case h
α : Type
inst✝ : Fintype α
X : Profinite
Z : α → Profinite
π : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : (forget Profinite).obj Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (y, (↑(CategoryTheory.inv β) (↑f y)).snd).snd =
    ↑(CategoryTheory.inv β) (↑f (y, (↑(CategoryTheory.inv β) (↑f y)).snd).fst)
Tactic:
rfl
State after:
no goals