Theorem: MyNat.le_trans (TheoremProvingLean/inductive_types.lean)

State before:
a b c : Nat
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
Tactic:
cases hab with
| intro d hd =>
  cases hbc with
  | intro e he =>
    exists d + e
    rw [he, hd]
    simp
State after:
no goals

State before:
case intro
a b c : Nat
hbc : b ≤ c
d : Nat
hd : b = a + d
⊢ a ≤ c
Tactic:
cases hbc with
| intro e he =>
  exists d + e
  rw [he, hd]
  simp
State after:
no goals

State before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a ≤ c
Tactic:
exists d + e
State after:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ c = a + (d + e)

State before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ c = a + (d + e)
Tactic:
rw [he, hd]
State after:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a + d + e = a + (d + e)

State before:
case intro.intro
a b c d : Nat
hd : b = a + d
e : Nat
he : c = b + e
⊢ a + d + e = a + (d + e)
Tactic:
simp
State after:
no goals