Theorem: CategoryTheory.ExtrDisc.compatibility (ExtrDisc/Pullback.lean)

State before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
⊢ δ hOpen f ≫ θ hOpen f ≫ η hOpen f = ζ hOpen f ≫ ε
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
State after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε

State before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
have := HasPullbackOpenEmbedding f (hOpen a)
State after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε

State before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫
      δ hOpen f ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
rw [← Category.assoc, δ, fromFiniteCoproduct, finiteCoproduct.ι_desc]
State after:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ Sigma.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε

State before:
Y : ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
X : ExtrDisc
i : (a : α) → Z a ⟶ X
hOpen : ∀ (a : α), OpenEmbedding ↑(i a)
f : Y ⟶ X
a : α
this : HasPullback f (i a)
⊢ Sigma.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ θ hOpen f ≫ η hOpen f =
    finiteCoproduct.ι (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(i a))).pt) a ≫ ζ hOpen f ≫ ε
Tactic:
simp [ε, ζ, θ, η, fromExplicit]
State after:
no goals