-- 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.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 a.fst c.fst = true ∧ (le c.fst a.fst = false ∨ a.snd ≤ c.snd)

Tactic:
refine ⟨trans _ _ _ ab₂ bc₂, ?_⟩

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

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
⊢ zipIdxLE le a b = true → zipIdxLE le b c = true → zipIdxLE le a c = true

Tactic:
simp only [zipIdxLE]

Result:
α : 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

Proof state:
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

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 a.fst c.fst = true ∧ (le c.fst a.fst = false ∨ a.snd ≤ c.snd)

Tactic:
refine ⟨trans _ _ _ ab₂ 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
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

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

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
h : 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 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

Tactic:
simp_all

Result:
no goals

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

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

Result:
no goals

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

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
h : 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.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

Tactic:
rcases h with (cb₂ | _)

Result:
case isTrue.isFalse.isTrue.h.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 = false
bc₂ : le b.fst c.fst = true
cb₂ : le c.fst b.fst = false
⊢ le c.fst a.fst = false

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

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
⊢ le c.fst ?m.33541 = true

Tactic:
simpa using ca₂

Result:
no goals

Proof state:
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

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
ab₂ : le a.fst b.fst = true
ba₂ : le b.fst a.fst = false
bc₂ : le b.fst c.fst = true
cb₂ : 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:
α : 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
cb₂ : le c.fst b.fst = false
ca₂ : ¬le c.fst a.fst = false
⊢ le ?m.32769 a.fst = true

Tactic:
simpa using ca₂

Result:
no goals

Proof state:
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

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

Result:
no goals