internlm/Lean-Github huggingface dataset:
Theorem: Profinite.extensivity_injective
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
⊢ R₁ = R₂
Tactic:
have himage : (ζ ≫ β) R₁ = (ζ ≫ β) R₂ := by
  rw [comm]; change f (σ R₁) = f (σ R₂); rw [hR]
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂
Tactic:
replace himage := congr_arg (inv β) himage
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂
Tactic:
change ((ζ ≫ β ≫ inv β) R₁) = ((ζ ≫ β ≫ inv β) R₂) at himage
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂
Tactic:
rw [IsIso.hom_inv_id, Category.comp_id] at himage
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑ζ R₁ = ↑ζ R₂
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
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 => 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
⊢ R₁ = R₂
Tactic:
obtain ⟨a₁, r₁, h₁⟩ := finiteCoproduct.ι_jointly_surjective R₁
Proof state after:
case intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₁
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
case intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₁
⊢ R₁ = R₂
Tactic:
obtain ⟨a₂, r₂, h₂⟩ := finiteCoproduct.ι_jointly_surjective R₂
Proof state after:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₂
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₂
⊢ R₁ = R₂
Tactic:
have ha₁ : a₁ = R₁.fst := (congrArg Sigma.fst h₁).symm
Proof state after:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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
⊢ R₁ = R₂
Tactic:
have ha₂ : a₂ = R₂.fst := (congrArg Sigma.fst h₂).symm
Proof state after:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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
⊢ R₁ = R₂
Tactic:
have ha : a₁ = a₂ := by rwa [ha₁, ha₂]
Proof state after:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₂
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
case intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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₂
this : R₁ ∈ Set.range ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂)
⊢ R₁ = R₂
Tactic:
obtain ⟨xr', hr'⟩ := this
Proof state after:
case intro.intro.intro.intro.intro
α : 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))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
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.ι (fun a => pullback f (π a)) a₂) xr' = R₁
⊢ R₁ = R₂