-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem zipIdxLE_total (total : ∀ a b, le a b || le b a)
    (a b : α × Nat) : zipIdxLE le a b || zipIdxLE le b a

Proof state:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
⊢ (false || false) = true

Tactic:
have := total a.1 b.1

Result:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
this : (le a.fst b.fst || le b.fst a.fst) = true
⊢ (false || false) = true

Proof state:
case isFalse.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
this : (le a.fst b.fst || le b.fst a.fst) = true
⊢ (false || false) = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue.isTrue
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : le a.fst b.fst = true
h✝ : le b.fst a.fst = true
⊢ (decide (a.snd ≤ b.snd) || decide (b.snd ≤ a.snd)) = true

Tactic:
simpa using Nat.le_total a.2 b.2

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
⊢ ((if le a.fst b.fst = true then if le b.fst a.fst = true then decide (a.snd ≤ b.snd) else true else false) ||
      if le b.fst a.fst = true then if le a.fst b.fst = true then decide (b.snd ≤ a.snd) else true else false) =
    true

Tactic:
split <;> split

Result:
case isTrue.isTrue
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : le a.fst b.fst = true
h✝ : le b.fst a.fst = true
⊢ (decide (a.snd ≤ b.snd) || decide (b.snd ≤ a.snd)) = true

case isTrue.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
⊢ (true || false) = true

case isFalse.isTrue
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : le b.fst a.fst = true
⊢ (false || true) = true

case isFalse.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
⊢ (false || false) = true

Proof state:
case isTrue.isFalse
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : le a.fst b.fst = true
h✝ : ¬le b.fst a.fst = true
⊢ (true || false) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
⊢ (zipIdxLE le a b || zipIdxLE le b a) = true

Tactic:
simp only [zipIdxLE]

Result:
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
⊢ ((if le a.fst b.fst = true then if le b.fst a.fst = true then decide (a.snd ≤ b.snd) else true else false) ||
      if le b.fst a.fst = true then if le a.fst b.fst = true then decide (b.snd ≤ a.snd) else true else false) =
    true

Proof state:
case isFalse.isTrue
α : Type u_1
le : α → α → Bool
total : ∀ (a b : α), (le a b || le b a) = true
a b : α × Nat
h✝¹ : ¬le a.fst b.fst = true
h✝ : le b.fst a.fst = true
⊢ (false || true) = true

Tactic:
simp

Result:
no goals