-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mem_merge {a : α} {xs ys : List α} : a ∈ merge xs ys le ↔ a ∈ xs ∨ a ∈ ys

Proof state:
case cons.cons.isFalse
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ a ∈ y :: (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ y :: ys

Tactic:
simp only [mem_cons, or_assoc, Bool.not_eq_true, ih, ← or_assoc]

Result:
case cons.cons.isFalse
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ ((a = y ∨ a = x) ∨ a ∈ xs) ∨ a ∈ ys ↔ ((a = x ∨ a ∈ xs) ∨ a = y) ∨ a ∈ ys

Proof state:
case cons.nil
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
⊢ a ∈ (x :: xs).merge [] le ↔ a ∈ x :: xs ∨ a ∈ []

Tactic:
simp [merge]

Result:
no goals

Proof state:
case cons.cons.isTrue
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : le x y = true
⊢ a ∈ x :: xs.merge (y :: ys) le ↔ a ∈ x :: xs ∨ a ∈ y :: ys

Tactic:
simp_all [or_assoc]

Result:
no goals

Proof state:
case cons.cons.isFalse
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ ((a = y ∨ a = x) ∨ a ∈ xs) ∨ a ∈ ys ↔ ((a = x ∨ a ∈ xs) ∨ a = y) ∨ a ∈ ys

Tactic:
apply or_congr_left

Result:
case cons.cons.isFalse.h
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ (a = y ∨ a = x) ∨ a ∈ xs ↔ (a = x ∨ a ∈ xs) ∨ a = y

Proof state:
case cons.cons
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
⊢ (a ∈ if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) ↔ a ∈ x :: xs ∨ a ∈ y :: ys

Tactic:
split <;> rename_i h

Result:
case cons.cons.isTrue
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : le x y = true
⊢ a ∈ x :: xs.merge (y :: ys) le ↔ a ∈ x :: xs ∨ a ∈ y :: ys

case cons.cons.isFalse
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ a ∈ y :: (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ y :: ys

Proof state:
case cons.cons.isFalse.h
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
h : ¬le x y = true
⊢ (a = y ∨ a = x) ∨ a ∈ xs ↔ (a = x ∨ a ∈ xs) ∨ a = y

Tactic:
simp only [or_comm (a := a = y), or_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
le : α → α → Bool
a : α
ys : List α
⊢ a ∈ [].merge ys le ↔ a ∈ [] ∨ a ∈ ys

Tactic:
simp [merge]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
⊢ a ∈ (x :: xs).merge (y :: ys) le ↔ a ∈ x :: xs ∨ a ∈ y :: ys

Tactic:
simp only [merge]

Result:
case cons.cons
α : Type u_1
le : α → α → Bool
a x : α
xs : List α
ih✝ : ∀ {ys : List α}, a ∈ xs.merge ys le ↔ a ∈ xs ∨ a ∈ ys
y : α
ys : List α
ih : a ∈ (x :: xs).merge ys le ↔ a ∈ x :: xs ∨ a ∈ ys
⊢ (a ∈ if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) ↔ a ∈ x :: xs ∨ a ∈ y :: ys