internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
have comm : ζ ≫ β = α ≫ f := by
   refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
   simp [← Category.assoc, finiteCoproduct.ι_desc, ExtrDisc.pullback.condition]
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
intro R₁ R₂ hR
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ R₁ = R₂
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ R₁ = R₂
Tactic:
have himage : (ζ ≫ β) R₁ = (ζ ≫ β) R₂ := by
  rw [comm]; change f (α R₁) = f (α R₂); rw [hR]
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
⊢ R₁ = R₂
Tactic:
replace himage := congr_arg (inv β) himage
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₁) = ↑(CategoryTheory.inv β) (↑(ζ ≫ β) R₂)
⊢ R₁ = R₂
Tactic:
change ((ζ ≫ β ≫ inv β) R₁) = ((ζ ≫ β ≫ inv β) R₂) at himage
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₁ = ↑(ζ ≫ β ≫ CategoryTheory.inv β) R₂
⊢ R₁ = R₂
Tactic:
rw [IsIso.hom_inv_id, Category.comp_id] at himage
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
⊢ R₁ = R₂
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
himage : ↑ζ R₁ = ↑ζ R₂
Hfst : R₁.fst = R₂.fst
⊢ R₁ = R₂
Tactic:
exact Sigma.subtype_ext Hfst hR
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ ζ ≫ β = α ≫ f
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
a : α✝
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ ζ ≫ β =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ α ≫ f
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
a : α✝
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ ζ ≫ β =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) a ≫ α ≫ f
Tactic:
simp [← Category.assoc, finiteCoproduct.ι_desc, ExtrDisc.pullback.condition]
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑(ζ ≫ β) R₁ = ↑(ζ ≫ β) R₂
Tactic:
rw [comm]
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = α ≫ f
R₁ R₂ : CoeSort.coe (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt)
hR :
  ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₁ =
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
          ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
      R₂
⊢ ↑(α ≫ f) R₁ = ↑(α ≫ f) R₂