internlm/Lean-Github huggingface dataset:
Theorem: Profinite.extensivity_injective
Proof state before:
case this
α : 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 => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
R₁ R₂ : (forget Profinite).obj (finiteCoproduct fun a => pullback f (π a))
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
a₁ : α
r₁ : ↑((fun a => pullback f (π a)) a₁).toCompHaus.toTop
h₁✝ : R₁ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₁) r₁
a₂ : α
r₂ : ↑((fun a => pullback f (π a)) a₂).toCompHaus.toTop
h₂ : R₂ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂
ha₁ : a₁ = R₁.fst
ha₂ : a₂ = R₂.fst
ha : a₁ = a₂
xr' : (forget Profinite).obj (pullback f (π a₂))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr') =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂)
hr' : ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr' = R₁
a : α
x y : (forget Profinite).obj (pullback f (π a))
h₁ : ↑(pullback.fst f (π a)) x = ↑(pullback.fst f (π a)) y
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
h' : ↑(pullback.snd f (π a) ≫ π a) y = ↑(pullback.snd f (π a) ≫ π a) x
r s : (forget Profinite).obj (Z a)
hrs✝ : ↑(π a) r = ↑(π a) s
hrs : ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r) = ↑(π a) s
hrs'✝ : ↑(π a) s = ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r)
hrs' :
  ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) s) =
    ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r)
this : Function.Injective ↑(finiteCoproduct.desc (fun a => Z a) π)
⊢ r = s
Tactic:
exact (finiteCoproduct.ι_injective a (this hrs')).symm
Proof state after:
no goals
Theorem: Profinite.extensivity_injective
Proof state before:
case this.hf
α : 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 => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
R₁ R₂ : (forget Profinite).obj (finiteCoproduct fun a => pullback f (π a))
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
a₁ : α
r₁ : ↑((fun a => pullback f (π a)) a₁).toCompHaus.toTop
h₁✝ : R₁ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₁) r₁
a₂ : α
r₂ : ↑((fun a => pullback f (π a)) a₂).toCompHaus.toTop
h₂ : R₂ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂
ha₁ : a₁ = R₁.fst
ha₂ : a₂ = R₂.fst
ha : a₁ = a₂
xr' : (forget Profinite).obj (pullback f (π a₂))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr') =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂)
hr' : ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr' = R₁
a : α
x y : (forget Profinite).obj (pullback f (π a))
h₁ : ↑(pullback.fst f (π a)) x = ↑(pullback.fst f (π a)) y
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
h' : ↑(pullback.snd f (π a) ≫ π a) y = ↑(pullback.snd f (π a) ≫ π a) x
r s : (forget Profinite).obj (Z a)
hrs✝ : ↑(π a) r = ↑(π a) s
hrs : ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r) = ↑(π a) s
hrs'✝ : ↑(π a) s = ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r)
hrs' :
  ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) s) =
    ↑(finiteCoproduct.desc (fun a => Z a) π) (↑(finiteCoproduct.ι (fun a => Z a) a) r)
⊢ Function.Bijective ↑(finiteCoproduct.desc (fun a => Z a) π)
Tactic:
exact ConcreteCategory.bijective_of_isIso _
Proof state after:
no goals
Theorem: Profinite.extensivity_injective
Proof state before:
case hf
α : 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 => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
R₁ R₂ : (forget Profinite).obj (finiteCoproduct fun a => pullback f (π a))
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
a₁ : α
r₁ : ↑((fun a => pullback f (π a)) a₁).toCompHaus.toTop
h₁✝ : R₁ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₁) r₁
a₂ : α
r₂ : ↑((fun a => pullback f (π a)) a₂).toCompHaus.toTop
h₂✝ : R₂ = ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂
ha₁ : a₁ = R₁.fst
ha₂ : a₂ = R₂.fst
ha : a₁ = a₂
xr' : (forget Profinite).obj (pullback f (π a₂))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr') =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
      (↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₂) r₂)
hr' : ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂) xr' = R₁
a : α
x y : (forget Profinite).obj (pullback f (π a))
h₁ : ↑(pullback.fst f (π a)) x = ↑(pullback.fst f (π a)) y
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
h' : ↑(pullback.snd f (π a) ≫ π a) y = ↑(pullback.snd f (π a) ≫ π a) x
this✝ : Function.Injective ↑(π a)
h₂ : ↑(pullback.snd f (π a)) y = ↑(pullback.snd f (π a)) x
this : ↑x = ↑y
⊢ x = y
Tactic:
exact Subtype.ext this
Proof state after:
no goals
Theorem: Profinite.extensivity_explicit
Proof 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 _ π
Proof 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))
Theorem: Profinite.extensivity_explicit
Proof 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 _
Proof 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))
Theorem: Profinite.extensivity_explicit
Proof 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 => _⟩
Proof 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
Theorem: Profinite.extensivity_explicit
Proof 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⟩
Proof 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}
Theorem: Profinite.extensivity_explicit
Proof 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
Proof 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}
Theorem: Profinite.extensivity_explicit
Proof 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
Proof 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)
Theorem: Profinite.extensivity_explicit
Proof 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
Proof 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
Theorem: Profinite.extensivity_explicit
Proof 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]
Proof state after:
no goals
Theorem: Profinite.extensivity_explicit
Proof 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
Proof 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
Theorem: Profinite.extensivity_explicit
Proof 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
Proof state after:
no goals
Theorem: Profinite.extensivity_explicit
Proof 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
Proof 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)
Theorem: Profinite.extensivity_explicit
Proof 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 β) _ = _
Proof 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)
Theorem: Profinite.extensivity_explicit
Proof 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]
Proof 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)
Theorem: Profinite.extensivity_explicit
Proof 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
Proof state after:
no goals
Theorem: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let θ := Sigma.mapIso (fun a => fromExplicitIso f (i a))
Proof state after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Theorem: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let δ := FromFiniteCoproductIso (fun a => Profinite.pullback f (i a))
Proof state after:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Theorem: Profinite.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
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
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Theorem: Profinite.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => pullback f (i a)) a ≫ δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => pullback f (i a)) a ≫
      finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Theorem: Profinite.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : Profinite
Z : α → Profinite
i : (a : α) → Z a ⟶ X
Y : Profinite
f : Y ⟶ X
H : IsIso (Sigma.desc i)
θ : (∐ fun a => pullback f (i a)) ≅ ∐ fun a => Limits.pullback f (i a) := Sigma.mapIso fun a => fromExplicitIso f (i a)
δ : (finiteCoproduct fun a => pullback f (i a)) ≅ ∐ fun a => pullback f (i a) :=
  FromFiniteCoproductIso fun a => pullback f (i a)
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => pullback f (i a)) a ≫ δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => pullback f (i a)) a ≫
      finiteCoproduct.desc (fun a => pullback f (i a)) fun a => pullback.fst f (i a)
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, fromExplicit]
Proof state after:
no goals