internlm/Lean-Github huggingface dataset:
Theorem: Profinite.extensivity_injective
Proof state before:
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₂
Tactic:
rw [← hr', h₂] at hR
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))
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₁
⊢ R₁ = R₂
Theorem: Profinite.extensivity_injective
Proof state before:
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))
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₁
hf :
  ∀ (a : α),
    Function.Injective
      ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a ≫
          finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
this : xr' = r₂
⊢ R₁ = R₂
Tactic:
rw [← hr', h₂, this]
Proof state after:
no goals
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) π
⊢ ζ ≫ β = σ ≫ f
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
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) π
a : α
⊢ finiteCoproduct.ι (fun a => pullback f (π a)) a ≫ ζ ≫ β = finiteCoproduct.ι (fun a => pullback f (π a)) a ≫ σ ≫ f
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) π
a : α
⊢ finiteCoproduct.ι (fun a => pullback f (π a)) a ≫ ζ ≫ β = finiteCoproduct.ι (fun a => pullback f (π a)) a ≫ σ ≫ f
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, pullback.condition]
Proof state after:
no goals
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:
rw [comm]
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₂
⊢ ↑(σ ≫ f) R₁ = ↑(σ ≫ f) 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₂
⊢ ↑(σ ≫ f) R₁ = ↑(σ ≫ f) R₂
Tactic:
change f (σ R₁) = f (σ R₂)
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₂
⊢ ↑f (↑σ R₁) = ↑f (↑σ 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₂
⊢ ↑f (↑σ R₁) = ↑f (↑σ R₂)
Tactic:
rw [hR]
Proof state after:
no goals
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₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
Tactic:
constructor <;> rfl
Proof state after:
no goals
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₂
this : (↑ζ R₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
⊢ R₁.fst = R₂.fst
Tactic:
rw [← this.1, ← this.2, himage]
Proof state after:
no goals
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
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
⊢ a₁ = a₂
Tactic:
rwa [ha₁, ha₂]
Proof state after:
no goals
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))
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₁ ∈ Set.range ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂)
Tactic:
rw [← finiteCoproduct.range_eq ha, h₁]
Proof state after:
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))
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₂
⊢ ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₁) r₁ ∈
    Set.range ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₁)
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))
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₂
⊢ ↑(finiteCoproduct.ι (fun a => (fun a => pullback f (π a)) a) a₁) r₁ ∈
    Set.range ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₁)
Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]
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 : α
⊢ Function.Injective ↑(pullback.fst f (π a))
Tactic:
intro x y h
Proof state after:
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
⊢ x = y
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
this : Function.Injective ↑(π a)
h₂ : ↑(pullback.snd f (π a)) y = ↑(pullback.snd f (π a)) x
⊢ ↑x = ↑y
Tactic:
exact Prod.ext h₁ h₂.symm
Proof state after:
no goals