Theorem: Profinite.extensivity_injective (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) π)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let ζ := finiteCoproduct.desc _ (fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a )
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
⊢ Function.Injective ↑(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 => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let σ := finiteCoproduct.desc _ ((fun a => pullback.fst f (π a)))
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)
⊢ Function.Injective ↑(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 => 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)
⊢ Function.Injective ↑(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 => 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) π
⊢ Function.Injective ↑(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 => 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) π
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
have comm : ζ ≫ β = σ ≫ f := by
   refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
   simp [← Category.assoc, finiteCoproduct.ι_desc, pullback.condition]
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
⊢ Function.Injective ↑(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 => 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
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
intro R₁ R₂ hR
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₂
⊢ R₁ = R₂

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]
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₂

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
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₂

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
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₂

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
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₂

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₁
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₂

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₂
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₂

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
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₂

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
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₂

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₂]
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₂

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₂
⊢ R₁ = R₂
Tactic:
have : R₁ ∈ Set.range (finiteCoproduct.ι _ a₂)
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₂
⊢ R₁ ∈ Set.range ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a₂)

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₂

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
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₂

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
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₂

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₁
⊢ R₁ = R₂
Tactic:
have hf : ∀ (a : α), Function.Injective 
    ((finiteCoproduct.ι _ a) ≫ (finiteCoproduct.desc _ ((fun a => pullback.fst f (π a)))))
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 : α),
    Function.Injective
      ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a ≫
          finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))

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))
⊢ R₁ = R₂

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))
⊢ R₁ = R₂
Tactic:
have := hf a₂ hR
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₁
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₂

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]
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 => 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 => _)
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

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]
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 => 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]
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₂

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₂)
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₂)

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]
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 => 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
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 => 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]
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 => 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₂]
State after:
no goals

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₁]
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₁)

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]
State after:
no goals

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
      ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a ≫
          finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
intro a
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 : α
⊢ Function.Injective
    ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a ≫
        finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))

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
    ↑(finiteCoproduct.ι (fun a => pullback f (π a)) a ≫
        finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
simp only [finiteCoproduct.ι_desc]
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 : α
⊢ Function.Injective ↑(pullback.fst f (π a))

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
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

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
⊢ x = y
Tactic:
have h₁ := h
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 h₁ : ↑(pullback.fst f (π a)) x = ↑(pullback.fst f (π a)) y
⊢ x = y

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 h₁ : ↑(pullback.fst f (π a)) x = ↑(pullback.fst f (π a)) y
⊢ x = y
Tactic:
apply_fun f at h
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
h : ↑f (↑(pullback.fst f (π a)) x) = ↑f (↑(pullback.fst f (π a)) y)
⊢ x = y

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 : ↑f (↑(pullback.fst f (π a)) x) = ↑f (↑(pullback.fst f (π a)) y)
⊢ x = y
Tactic:
change (pullback.fst f (π a) ≫ f) x = _ at h
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
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
⊢ x = y

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)
⊢ x = y
Tactic:
have h' := h.symm
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
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
h' : ↑f (↑(pullback.fst f (π a)) y) = ↑(pullback.fst f (π a) ≫ f) x
⊢ x = y

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' : ↑f (↑(pullback.fst f (π a)) y) = ↑(pullback.fst f (π a) ≫ f) x
⊢ x = y
Tactic:
change (pullback.fst f (π a) ≫ f) y = _ at h'
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
h : ↑(pullback.fst f (π a) ≫ f) x = ↑f (↑(pullback.fst f (π a)) y)
h' : ↑(pullback.fst f (π a) ≫ f) y = ↑(pullback.fst f (π a) ≫ f) x
⊢ x = y

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.fst f (π a) ≫ f) y = ↑(pullback.fst f (π a) ≫ f) x
⊢ x = y
Tactic:
rw [pullback.condition] at h'
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
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
⊢ x = y

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
⊢ x = y
Tactic:
have : Function.Injective (π a)
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))
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
⊢ Function.Injective ↑(π a)

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)
⊢ x = y

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)
⊢ x = y
Tactic:
have h₂ := this h'
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
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

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
⊢ x = y
Tactic:
suffices : x.val = y.val
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
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

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

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
State after:
no goals

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
⊢ Function.Injective ↑(π a)
Tactic:
intro r s hrs
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))
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
⊢ r = s

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
⊢ r = s
Tactic:
rw [← finiteCoproduct.ι_desc_apply] at hrs
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))
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
⊢ r = s

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
⊢ r = s
Tactic:
have hrs' := hrs.symm
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))
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)
⊢ r = s

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)
⊢ r = s
Tactic:
rw [← finiteCoproduct.ι_desc_apply] at hrs'
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))
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)
⊢ r = s

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)
⊢ r = s
Tactic:
have : Function.Injective (finiteCoproduct.desc (fun a ↦ Z a) π)
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))
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.Injective ↑(finiteCoproduct.desc (fun a => Z a) π)

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

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
State after:
no goals

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)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => Z a) π)
Tactic:
apply Function.Bijective.injective
State after:
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) π)

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 _
State after:
no goals

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
State after:
no goals