Theorem: Sinf.var_refl (SInfinity/Lemmas.lean)

State before:
a : String
⊢ Ø ⋁ ∀ₛ a ; _ a =ₛ _ a
Tactic:
apply S_induction
State after:
case a
a : String
⊢ ∀ (n : ℕ), Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]

State before:
case a
a : String
⊢ ∀ (n : ℕ), Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Tactic:
intros n
State after:
case a
a : String
n : ℕ
⊢ Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]

State before:
case a
a : String
n : ℕ
⊢ Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Tactic:
constructor <;> simp <;> try rw [String.decEq_refl a] <;> apply NoVars.fromNat
State after:
case a.a
a : String
n : ℕ
⊢ Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat))) =
    Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat)))

State before:
case a.a
a : String
n : ℕ
⊢ Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat))) =
    Sinf_const.eval
      (Sinf_const.coerce
        (match String.decEq a a with
        | isTrue h => fromNat n
        | isFalse h => _ a)
        (id
          (Eq.mpr
            (_ :
              NoVars
                  (match String.decEq a a with
                  | isTrue h => fromNat n
                  | isFalse h => _ a) =
                NoVars
                  (match isTrue (_ : a = a) with
                  | isTrue h => fromNat n
                  | isFalse h => _ a))
            NoVars.fromNat)))
Tactic:
rfl
State after:
no goals

State before:
case a.nv₂
a : String
n : ℕ
⊢ NoVars
    (match String.decEq a a with
    | isTrue h => fromNat n
    | isFalse h => _ a)
Tactic:
rw [String.decEq_refl a] <;> apply NoVars.fromNat
State after:
no goals