α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x x_1 => x = x_1) a b
⊢ a ∈ c₂
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a1 : a ∈ c₁
⊢ a ∈ c₂
let ⟨b, b2, ab⟩ := h1 a1
no goals
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x x_1 => x = x_1) a b
⊢ a ∈ c₂
rwa [ab]
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x x_1 => x = x_1) b a
⊢ a ∈ c₁
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a2 : a ∈ c₂
⊢ a ∈ c₁
let ⟨b, b1, ab⟩ := h2 a2
no goals
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
x✝ : LiftRel (fun x x_1 => x = x_1) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x x_1 => x = x_1) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x x_1 => x = x_1) a b
a2 : a ∈ c₂
b : α
b1 : b ∈ c₁
ab : (fun x x_1 => x = x_1) b a
⊢ a ∈ c₁
rwa [← ab]