E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (Nat.find (_ : ∃ a, x a ≠ y a)) ≠ y (Nat.find (_ : ∃ a, x a ≠ y a))
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (firstDiff x y) ≠ y (firstDiff x y)
rw [firstDiff_def, dif_pos h]
no goals
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (Nat.find (_ : ∃ a, x a ≠ y a)) ≠ y (Nat.find (_ : ∃ a, x a ≠ y a))
exact Nat.find_spec (ne_iff.1 h)