no goals
α : Type u
A : α → PSet
y : PSet
x✝ : y ∈ ⋃₀ mk α A
a : Type (mk α A)
c : Type (Func (mk α A) a)
e : Equiv y (Func (A a) c)
this : Func (A a) c ∈ mk (Type (A a)) (Func (A a))
⊢ Func (A a) c ∈ A (?m.27126 α A y x✝ a c e this)
rwa [eta] at this
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (mk (Type (A a)) (Func (A a)))
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (A a)
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
rw [← eta (A a)] at e
no goals
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (mk (Type (A a)) (Func (A a)))
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
exact
  let ⟨βt, _⟩ := e
  let ⟨c, bc⟩ := βt b
  ⟨⟨a, c⟩, yb.trans bc⟩