case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y

case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y
constructor <;> intro h
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y
intro a h' b
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
have h := h b
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp] at h
no goals
case mp
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y
apply h _ h'
case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y
intro b h'
case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ a, a ∈ x ∧ b ∈ f a
⊢ b ∈ y
case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h'
case mpr.intro.intro
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y
case mpr
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ a, a ∈ x ∧ b ∈ f a
⊢ b ∈ y
rcases h' with ⟨a, h₀, h₁⟩
no goals
case mpr.intro.intro
α✝ : Type ?u.51205
β : Type u_1
γ : Type ?u.51211
α : Type u_1
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y
apply h _ h₀ _ h₁