Theorem: Char.utf8Size_pos (Metamath/Verify.lean)

State before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 1 utf8Size.proof_2
Tactic:
decide
State after:
no goals

State before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 2 utf8Size.proof_4
Tactic:
decide
State after:
no goals

State before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 3 utf8Size.proof_6
Tactic:
decide
State after:
no goals

State before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
Tactic:
decide
State after:
no goals