E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < if h : x ≠ y then Nat.find (_ : ∃ a, x a ≠ y a) else 0
⊢ x n = y n
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < firstDiff x y
⊢ x n = y n
rw [firstDiff_def] at hn
case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find (_ : ∃ a, x a ≠ y a)
⊢ x n = y n

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : ¬x ≠ y
hn : n < 0
⊢ x n = y n
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n < if h : x ≠ y then Nat.find (_ : ∃ a, x a ≠ y a) else 0
⊢ x n = y n
split_ifs at hn with h
case a
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find (_ : ∃ a, x a ≠ y a)
⊢ x n = y n ↔ ¬x n ≠ y n
case inl
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find (_ : ∃ a, x a ≠ y a)
⊢ x n = y n
convert Nat.find_min (ne_iff.1 h) hn
no goals
case a
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : x ≠ y
hn : n < Nat.find (_ : ∃ a, x a ≠ y a)
⊢ x n = y n ↔ ¬x n ≠ y n
simp
no goals
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
h : ¬x ≠ y
hn : n < 0
⊢ x n = y n
exact (not_lt_zero' hn).elim