Theorem: Waffle.le_trans (PnP2023/Lec_01_25/Answer.lean)

State before:
a b c : Answer
⊢ a ≤ b → b ≤ c → a ≤ c
Tactic:
intro h₁ h₂
State after:
a b c : Answer
h₁ : a ≤ b
h₂ : b ≤ c
⊢ a ≤ c

State before:
a b c : Answer
h₁ : a ≤ b
h₂ : b ≤ c
⊢ a ≤ c
Tactic:
cases c₁:h₁
State after:
case no_le
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c

case le_yes
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c

case refl
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c

State before:
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c
Tactic:
case no_le => 
  apply Answer.le.no_le
State after:
no goals

State before:
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
case le_yes => 
  cases c₂:h₂
  case le_yes => apply Answer.le.le_yes
  case refl => assumption
State after:
no goals

State before:
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
case refl => assumption
State after:
no goals

State before:
b c : Answer
h₂ : b ≤ c
h₁ : Answer.no ≤ b
c₁ : h₁ = ⋯
⊢ Answer.no ≤ c
Tactic:
apply Answer.le.no_le
State after:
no goals

State before:
a c : Answer
h₁ : a ≤ Answer.yes
h₂ : Answer.yes ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
cases c₂:h₂
State after:
case le_yes
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes

case refl
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes

State before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
case le_yes => apply Answer.le.le_yes
State after:
no goals

State before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
case refl => assumption
State after:
no goals

State before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
apply Answer.le.le_yes
State after:
no goals

State before:
a : Answer
h₁ : a ≤ Answer.yes
c₁ : h₁ = ⋯
h₂ : Answer.yes ≤ Answer.yes
c₂ : h₂ = ⋯
⊢ a ≤ Answer.yes
Tactic:
assumption
State after:
no goals

State before:
a c : Answer
h₁ : a ≤ a
h₂ : a ≤ c
c₁ : h₁ = ⋯
⊢ a ≤ c
Tactic:
assumption
State after:
no goals