α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) ↔ p ∧ ∃ h, get o h = a
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o
dsimp [restrict, mem_eq]
case mp
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) → p ∧ ∃ h, get o h = a

case mpr
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, get o h = a) → ∃ h_1, get o (_ : o.Dom) = a
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) ↔ p ∧ ∃ h, get o h = a
constructor
case mpr.intro.intro
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : get o w✝ = a
⊢ ∃ h_1, get o (_ : o.Dom) = a
case mpr
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, get o h = a) → ∃ h_1, get o (_ : o.Dom) = a
rintro ⟨h₀, _, h₂⟩
no goals
case mpr.intro.intro
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : get o w✝ = a
⊢ ∃ h_1, get o (_ : o.Dom) = a
exact ⟨h₀, h₂⟩
case mp.intro
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : get o (_ : o.Dom) = a
⊢ p ∧ ∃ h, get o h = a
case mp
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) → p ∧ ∃ h, get o h = a
rintro ⟨h₀, h₁⟩
no goals
case mp.intro
α : Type u_1
β : Type ?u.52027
γ : Type ?u.52030
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : get o (_ : o.Dom) = a
⊢ p ∧ ∃ h, get o h = a
exact ⟨h₀, ⟨_, h₁⟩⟩