α : Type u_1
β : Type ?u.81876
γ : Type ?u.81879
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb
α : Type u_1
β : Type ?u.81876
γ : Type ?u.81879
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b
simp [inter_def]
no goals
α : Type u_1
β : Type ?u.81876
γ : Type ?u.81879
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb
aesop