case h
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x✝ : α₂
⊢ ↑(↑(embeddingCongr ea ec) (Embedding.trans f g)) x✝ =
    ↑(Embedding.trans (↑(embeddingCongr ea eb) f) (↑(embeddingCongr eb ec) g)) x✝
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ ↑(embeddingCongr ea ec) (Embedding.trans f g) =
    Embedding.trans (↑(embeddingCongr ea eb) f) (↑(embeddingCongr eb ec) g)
ext
no goals
case h
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x✝ : α₂
⊢ ↑(↑(embeddingCongr ea ec) (Embedding.trans f g)) x✝ =
    ↑(Embedding.trans (↑(embeddingCongr ea eb) f) (↑(embeddingCongr eb ec) g)) x✝
simp