-- 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:
α : 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
⊢ False

Tactic:
simp_all [trans _ _ _ (by simpa using ca₂) ab₂]

Result:
no goals

Proof state:
case isTrue.isTrue.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
⊢ decide (a.snd ≤ b.snd) = 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
⊢ 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)

Tactic:
intro ab₁

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
ab₁ : 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.isFalse.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
⊢ true = 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.isFalse.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 = false
bc₂ : le b.fst c.fst = true
⊢ 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.isFalse.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 = false
bc₂ : le b.fst c.fst = true
h : le c.fst b.fst = false ∨ b.snd ≤ c.snd
⊢ le c.fst a.fst = false ∨ a.snd ≤ c.snd

Tactic:
left

Result:
case isTrue.isFalse.isTrue.h
α : 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 : le c.fst b.fst = false ∨ b.snd ≤ c.snd
⊢ le c.fst a.fst = false

Proof state:
case isFalse.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 c.fst = true
bc₂ : ¬le a.fst c.fst = true
⊢ false = true → false = true → false = true

Tactic:
simp_all

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
⊢ (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) = true →
    (if le b.fst c.fst = true then if le c.fst b.fst = true then decide (b.snd ≤ c.snd) else true else 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:
split <;> split <;> split <;> rename_i ab₂ ba₂ bc₂

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
⊢ 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

case isTrue.isTrue.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
⊢ decide (a.snd ≤ b.snd) = 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

case isTrue.isFalse.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
⊢ true = 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

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

case isFalse.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 c.fst = true
bc₂ : le c.fst b.fst = true
⊢ false = true →
    decide (b.snd ≤ c.snd) = 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

case isFalse.isTrue.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 c.fst = true
bc₂ : ¬le c.fst b.fst = true
⊢ false = true →
    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

case isFalse.isFalse.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 c.fst = true
bc₂ : le a.fst c.fst = true
⊢ false = true → false = true → (if le c.fst a.fst = true then decide (a.snd ≤ c.snd) else true) = true

case isFalse.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 c.fst = true
bc₂ : ¬le a.fst c.fst = true
⊢ false = true → false = true → false = true

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 = false
bc₂ : le b.fst c.fst = true
h✝ : b.snd ≤ c.snd
ca₂ : ¬le c.fst a.fst = false
⊢ False

Tactic:
simp_all [trans _ _ _ bc₂ (by simpa using ca₂)]

Result:
no goals