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) π
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₂
Tactic:
change f (α R₁) = f (α R₂)
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₂)
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₂
⊢ ↑f (↑α R₁) = ↑f (↑α R₂)
Tactic:
rw [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) π
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₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
Tactic:
constructor <;> rfl
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₂
himage : ↑ζ R₁ = ↑ζ R₂
this : (↑ζ R₁).fst = R₁.fst ∧ (↑ζ R₂).fst = R₂.fst
⊢ R₁.fst = R₂.fst
Tactic:
rw [← this.1, ← this.2, himage]
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_explicit
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)
⊢ IsIso
    (finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let β := finiteCoproduct.desc _ π
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso
    (finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ IsIso
    (finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
refine' isIso_of_bijective ⟨extensivity_injective f HIso hOpen, fun y => _⟩
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ∃ a,
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
            ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
        a =
      y
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ∃ a,
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
            ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
        a =
      y
Tactic:
refine' ⟨⟨(inv β (f y)).1, ⟨y, (inv β (f y)).2, _⟩⟩, rfl⟩
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Tactic:
have inj : Function.Injective (inv β) := by intros r s hrs
  convert congr_arg β hrs <;> change _ = (inv β ≫ β) _<;> simp only [IsIso.inv_hom_id]<;> rfl
Proof state after:
α : Type
inst✝ : Fintype α
X : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd = ↑f y
Tactic:
apply inj
Proof state after:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd) =
    ↑(CategoryTheory.inv β) (↑f y)
Theorem: ExtrDisc.extensivity_explicit
Proof state before:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
⊢ ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Tactic:
intro a
Proof state after:
case a
α : Type
inst✝ : Fintype α
X : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
a : α
⊢ π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Theorem: ExtrDisc.extensivity_explicit
Proof state before:
case a
α : 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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
a : α
⊢ π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
Tactic:
simp only [IsIso.comp_inv_eq, finiteCoproduct.ι_desc]
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
⊢ Function.Injective ↑(CategoryTheory.inv β)
Tactic:
intros r s hrs
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
r s : CoeSort.coe X
hrs : ↑(CategoryTheory.inv β) r = ↑(CategoryTheory.inv β) s
⊢ r = s
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
r s : CoeSort.coe X
hrs : ↑(CategoryTheory.inv β) r = ↑(CategoryTheory.inv β) s
⊢ r = s
Tactic:
convert congr_arg β hrs <;> change _ = (inv β ≫ β) _<;> simp only [IsIso.inv_hom_id]<;> rfl
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(CategoryTheory.inv β) (↑(π (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd) =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
change (_ ≫ inv β) _ = _
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(π (↑(CategoryTheory.inv β) (↑f y)).fst ≫ CategoryTheory.inv β) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
rw [this]
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Theorem: ExtrDisc.extensivity_explicit
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 => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
y : CoeSort.coe Y
inj : Function.Injective ↑(CategoryTheory.inv β)
this : ∀ (a : α), π a ≫ CategoryTheory.inv β = finiteCoproduct.ι Z a
⊢ ↑(finiteCoproduct.ι Z (↑(CategoryTheory.inv β) (↑f y)).fst) (↑(CategoryTheory.inv β) (↑f y)).snd =
    ↑(CategoryTheory.inv β) (↑f y)
Tactic:
rfl
Proof state after:
no goals
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
have hOpen := openEmbedding_of_sigma_desc_iso H
Proof state after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let θ := Sigma.mapIso (fun a => fromExplicitIso f (hOpen a))
Proof state after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
⊢ IsIso (Sigma.desc fun x => Limits.pullback.fst)
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
let δ := FromFiniteCoproductIso (fun a => (OpenEmbeddingCone f (hOpen a)).pt)
Proof state after:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
⊢ IsIso (θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Theorem: ExtrDisc.extensivity
Proof state before:
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ IsIso (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst)
Tactic:
convert extensivity_explicit f HIso hOpen
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))
Theorem: ExtrDisc.extensivity
Proof state before:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
⊢ (δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
      ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
case h.e'_5
α : Type
x✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
H : IsIso (Sigma.desc i)
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
θ : (∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅ ∐ fun a => pullback f (i a) :=
  Sigma.mapIso fun a => fromExplicitIso f (_ : OpenEmbedding ↑(i a))
δ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) ≅
  ∐ fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt :=
  FromFiniteCoproductIso fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) i)
a : α
⊢ (finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ.hom ≫ θ.hom ≫ Sigma.desc fun x => Limits.pullback.fst) =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(i a))