-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem zipIdxLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
    (a b c : α × Nat) : zipIdxLE le a b → zipIdxLE le b c → zipIdxLE le a c

Proof state:
case isTrue.isTrue.isTrue
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
⊢ decide (a.snd ≤ b.snd) = true →
    (if le c.fst b.fst = true then decide (b.snd ≤ c.snd) else true) = true →
      (if le a.fst c.fst = true then if le c.fst a.fst = true then decide (a.snd ≤ c.snd) else true else false) = true

Tactic:
simp_all

Result:
case isTrue.isTrue.isTrue
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
⊢ a.snd ≤ b.snd →
    le c.fst b.fst = false ∨ b.snd ≤ c.snd → le a.fst c.fst = true ∧ (le c.fst a.fst = false ∨ a.snd ≤ c.snd)

Proof state:
case isTrue.isTrue.isTrue.inr
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
ab₁ : a.snd ≤ b.snd
bc₁ : b.snd ≤ c.snd
⊢ le c.fst a.fst = false ∨ a.snd ≤ c.snd

Tactic:
exact Or.inr (Nat.le_trans ab₁ bc₁)

Result:
no goals

Proof state:
case isTrue.isFalse.isTrue.h.inr
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = false
bc₂ : le b.fst c.fst = true
h✝ : b.snd ≤ c.snd
⊢ le c.fst a.fst = false

Tactic:
exact (Decidable.byContradiction
  (fun ca₂ => by simp_all [trans _ _ _ bc₂ (by simpa using ca₂)]))

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
ab₁ : a.snd ≤ b.snd
cd₂ : le c.fst b.fst = false
ca₂ : ¬le c.fst a.fst = false
⊢ le ?m.26861 a.fst = true

Tactic:
simpa using ca₂

Result:
no goals

Proof state:
case isTrue.isFalse.isFalse
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : ¬le b.fst a.fst = true
bc₂ : ¬le b.fst c.fst = true
⊢ true = true →
    false = true →
      (if le a.fst c.fst = true then if le c.fst a.fst = true then decide (a.snd ≤ c.snd) else true else false) = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isTrue.isTrue.isTrue
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
ab₁ : a.snd ≤ b.snd
h : le c.fst b.fst = false ∨ b.snd ≤ c.snd
⊢ le c.fst a.fst = false ∨ a.snd ≤ c.snd

Tactic:
rcases h with (cd₂ | bc₁)

Result:
case isTrue.isTrue.isTrue.inl
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
ab₁ : a.snd ≤ b.snd
cd₂ : le c.fst b.fst = false
⊢ le c.fst a.fst = false ∨ a.snd ≤ c.snd

case isTrue.isTrue.isTrue.inr
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
a b c : α × Nat
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = true
bc₂ : le b.fst c.fst = true
ab₁ : a.snd ≤ b.snd
bc₁ : b.snd ≤ c.snd
⊢ le c.fst a.fst = false ∨ a.snd ≤ c.snd