case hs.h.mk
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_1
ε : Type u_2
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_1
ε : Type u_2
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
⊢ LocalEquiv.trans (prod e e') (prod f f') = prod (LocalEquiv.trans e f) (LocalEquiv.trans e' f')
ext ⟨x, y⟩ <;> simp [ext_iff]
no goals
case hs.h.mk
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
η : Type u_1
ε : Type u_2
e : LocalEquiv α β
f : LocalEquiv β γ
e' : LocalEquiv δ η
f' : LocalEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source
tauto