Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case var.true
a✝ : Nat
⊢ Ordering

pp: case var.false
a✝ : Nat
⊢ Ordering

pp: case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.var
a✝ : Nat
⊢ Ordering

pp: case true.false
⊢ Ordering

pp: case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.var
a✝ : Nat
⊢ Ordering

pp: case false.true
⊢ Ordering

pp: case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.and'
a✝⁵ : AndKind
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case or.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
case and'.and' ap p₁ p₂ aq q₁ q₂ => exact (ap.cmp aq).then <| (p₁.cmp q₁).then (p₂.cmp q₂)

Goal state after:
case var.true
a✝ : Nat
⊢ Ordering

case var.false
a✝ : Nat
⊢ Ordering

case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

case true.var
a✝ : Nat
⊢ Ordering

case true.false
⊢ Ordering

case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case true.or
a✝¹ a✝ : IProp
⊢ Ordering

case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

case false.var
a✝ : Nat
⊢ Ordering

case false.true
⊢ Ordering

case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case false.or
a✝¹ a✝ : IProp
⊢ Ordering

case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case or.true
a✝¹ a✝ : IProp
⊢ Ordering

case or.false
a✝¹ a✝ : IProp
⊢ Ordering

case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case or.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

case imp.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering