α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
⊢ x✝¹ = x✝
let ⟨L₁, hx, hy⟩ := Red.exact.1 H
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝
simp [Red.singleton_iff] at hx hy
no goals
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝
aesop