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

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

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

State before:
case a
a : String
n : ℕ
⊢ Ø ⋁ (¬ₛ _ a↗ =ₛ O) [a ≔ fromNat n]
Tactic:
induction n <;> simp at *
State after:
case a.zero
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O

case a.succ
a : String
n✝ : ℕ
n_ih✝ :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n✝
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n✝↗
          | isFalse h => _ a)↗ =ₛ
        O

State before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
case a.zero =>
  rw [String.decEq_refl a]; simp
  constructor <;> try constructor <;> try constructor
  intros p
  contradiction
State after:
no goals

State before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
case a.succ n ih =>
  rw [String.decEq_refl a] at *; simp at *
  cases ih
  case S_axiom_neg nv1 nv2 e =>
    constructor <;> try constructor <;> try assumption
    intros p
    contradiction
State after:
no goals

State before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
rw [String.decEq_refl a]
State after:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O

State before:
a : String
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => O
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
simp
State after:
a : String
⊢ Ø ⋁ ¬ₛ O↗ =ₛ O

State before:
a : String
⊢ Ø ⋁ ¬ₛ O↗ =ₛ O
Tactic:
constructor <;> try constructor <;> try constructor
State after:
case a
a : String
⊢ Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)

State before:
case a
a : String
⊢ Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Tactic:
intros p
State after:
case a
a : String
p : Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False

State before:
case a
a : String
p : Sinf_const.eval (Sinf_const.coerce (O↗) (NoVars.S NoVars.O)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case nv₂
a : String
⊢ NoVars O
Tactic:
constructor <;> try constructor
State after:
no goals

State before:
case nv₁.a
a : String
⊢ NoVars O
Tactic:
constructor
State after:
no goals

State before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match String.decEq a a with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
rw [String.decEq_refl a] at *
State after:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O

State before:
a : String
n : ℕ
ih :
  Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a)↗ =ₛ
        O
⊢ Ø ⋁
    ¬ₛ
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n↗
          | isFalse h => _ a)↗ =ₛ
        O
Tactic:
simp at *
State after:
a : String
n : ℕ
ih : Ø ⋁ ¬ₛ fromNat n↗ =ₛ O
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O

State before:
a : String
n : ℕ
ih : Ø ⋁ ¬ₛ fromNat n↗ =ₛ O
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
cases ih
State after:
case S_axiom_neg
a : String
n : ℕ
nv₁✝ : NoVars (fromNat n↗)
nv₂✝ : NoVars O
a✝ : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv₁✝) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂✝)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O

State before:
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
case S_axiom_neg nv1 nv2 e =>
  constructor <;> try constructor <;> try assumption
  intros p
  contradiction
State after:
no goals

State before:
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Ø ⋁ ¬ₛ fromNat n↗↗ =ₛ O
Tactic:
constructor <;> try constructor <;> try assumption
State after:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)

State before:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) ≠ Sinf_const.eval (Sinf_const.coerce O NoVars.O)
Tactic:
intros p
State after:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
p : Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False

State before:
case a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
p : Sinf_const.eval (Sinf_const.coerce (fromNat n↗↗) (NoVars.S nv1)) = Sinf_const.eval (Sinf_const.coerce O NoVars.O)
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case nv₂
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ NoVars O
Tactic:
constructor <;> try assumption
State after:
no goals

State before:
case nv₁.a
a : String
n : ℕ
nv1 : NoVars (fromNat n↗)
nv2 : NoVars O
e : Sinf_const.eval (Sinf_const.coerce (fromNat n↗) nv1) ≠ Sinf_const.eval (Sinf_const.coerce O nv2)
⊢ NoVars (fromNat n↗)
Tactic:
assumption
State after:
no goals