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

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

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

State before:
case a
a b : String
n : ℕ
⊢ Ø ⋁ (∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a) [a ≔ fromNat n]
Tactic:
simp
State after:
case a
a b : String
n : ℕ
⊢ Ø ⋁
    match String.decEq a b with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a

State before:
case a
a b : String
n : ℕ
⊢ Ø ⋁
    match String.decEq a b with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match String.decEq a b with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
Tactic:
cases (String.decEq a b)
State after:
case a.isFalse
a b : String
n : ℕ
h✝ : ¬a = b
⊢ Ø ⋁
    match isFalse h✝ with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isFalse h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isFalse h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a

case a.isTrue
a b : String
n : ℕ
h✝ : a = b
⊢ Ø ⋁
    match isTrue h✝ with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isTrue h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isTrue h✝ with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a

State before:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    match isFalse nab with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isFalse nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isFalse nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
Tactic:
case a.isFalse nab =>
  simp
  rw [String.decEq_refl a]; simp
  apply S_induction; intros m; simp
  rw [String.decEq_refl b]; simp
  induction n <;> induction m <;> simp at *
  case a.zero.zero =>
    constructor <;> constructor <;> constructor
  case a.zero.succ n ih =>
    rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
    constructor <;> try constructor <;> try constructor <;> try assumption
    simp at *
  case a.succ.zero n ih =>
    rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
    constructor <;> try constructor <;> try constructor <;> try assumption
    simp at *
  case a.succ.succ n m ihn ihm =>
    sorry
State after:
no goals

State before:
a b : String
n : ℕ
ab : a = b
⊢ Ø ⋁
    match isTrue ab with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isTrue ab with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isTrue ab with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
Tactic:
case a.isTrue ab =>
  simp; rw [ab]
  apply S_induction; simp
  rw [String.decEq_refl b]; simp
  intros n; constructor <;> constructor <;> apply NoVars.fromNat
State after:
no goals

State before:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    match isFalse nab with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isFalse nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isFalse nab with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
Tactic:
simp
State after:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    ∀ₛ b ;
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a) +ₛ
          _ b =ₛ
        _ b +ₛ
          match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a

State before:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    ∀ₛ b ;
      (match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a) +ₛ
          _ b =ₛ
        _ b +ₛ
          match String.decEq a a with
          | isTrue h => fromNat n
          | isFalse h => _ a
Tactic:
rw [String.decEq_refl a]
State after:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    ∀ₛ b ;
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a) +ₛ
          _ b =ₛ
        _ b +ₛ
          match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a

State before:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁
    ∀ₛ b ;
      (match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a) +ₛ
          _ b =ₛ
        _ b +ₛ
          match isTrue (_ : a = a) with
          | isTrue h => fromNat n
          | isFalse h => _ a
Tactic:
simp
State after:
a b : String
n : ℕ
nab : ¬a = b
⊢ Ø ⋁ ∀ₛ b ; fromNat n +ₛ _ b =ₛ _ b +ₛ fromNat n

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

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

State before:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁ fromNat n +ₛ _ b =ₛ _ b +ₛ fromNat n [b ≔ fromNat m]
Tactic:
simp
State after:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)

State before:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match String.decEq b b with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)
Tactic:
rw [String.decEq_refl b]
State after:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)

State before:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁
    (Sinf_term.subst (fromNat n) b (fromNat m) +ₛ
        match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) =ₛ
      (match isTrue (_ : b = b) with
        | isTrue h => fromNat m
        | isFalse h => _ b) +ₛ
        Sinf_term.subst (fromNat n) b (fromNat m)
Tactic:
simp
State after:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b (fromNat m) +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m)

State before:
case a
a b : String
n : ℕ
nab : ¬a = b
m : ℕ
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b (fromNat m) +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m)
Tactic:
induction n <;> induction m <;> simp at *
State after:
case a.zero.zero
a b : String
nab : ¬a = b
⊢ Ø ⋁ O +ₛ O =ₛ O +ₛ O

case a.zero.succ
a b : String
nab : ¬a = b
n✝ : ℕ
n_ih✝ : Ø ⋁ O +ₛ fromNat n✝ =ₛ fromNat n✝ +ₛ O
⊢ Ø ⋁ O +ₛ fromNat n✝↗ =ₛ fromNat n✝↗ +ₛ O

case a.succ.zero
a b : String
nab : ¬a = b
n✝ : ℕ
n_ih✝ : Ø ⋁ Sinf_term.subst (fromNat n✝) b O +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n✝) b O
⊢ Ø ⋁ Sinf_term.subst (fromNat n✝) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n✝) b O↗

case a.succ.succ
a b : String
nab : ¬a = b
n✝¹ n✝ : ℕ
n_ih✝¹ :
  Ø ⋁
      Sinf_term.subst (fromNat n✝¹) b (fromNat n✝) +ₛ fromNat n✝ =ₛ
        fromNat n✝ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝) →
    Ø ⋁
      Sinf_term.subst (fromNat n✝¹) b (fromNat n✝)↗ +ₛ fromNat n✝ =ₛ
        fromNat n✝ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝)↗
n_ih✝ :
  Ø ⋁
    Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗) +ₛ fromNat n✝↗ =ₛ
      fromNat n✝↗ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)
⊢ Ø ⋁
    Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)↗ +ₛ fromNat n✝↗ =ₛ
      fromNat n✝↗ +ₛ Sinf_term.subst (fromNat n✝¹) b (fromNat n✝↗)↗

State before:
a b : String
nab : ¬a = b
⊢ Ø ⋁ O +ₛ O =ₛ O +ₛ O
Tactic:
case a.zero.zero =>
  constructor <;> constructor <;> constructor
State after:
no goals

State before:
a b : String
nab : ¬a = b
n : ℕ
ih : Ø ⋁ O +ₛ fromNat n =ₛ fromNat n +ₛ O
⊢ Ø ⋁ O +ₛ fromNat n↗ =ₛ fromNat n↗ +ₛ O
Tactic:
case a.zero.succ n ih =>
  rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
  constructor <;> try constructor <;> try constructor <;> try assumption
  simp at *
State after:
no goals

State before:
a b : String
nab : ¬a = b
n : ℕ
ih : Ø ⋁ Sinf_term.subst (fromNat n) b O +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗
Tactic:
case a.succ.zero n ih =>
  rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
  constructor <;> try constructor <;> try constructor <;> try assumption
  simp at *
State after:
no goals

State before:
a b : String
nab : ¬a = b
n m : ℕ
ihn :
  Ø ⋁ Sinf_term.subst (fromNat n) b (fromNat m) +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m) →
    Ø ⋁
      Sinf_term.subst (fromNat n) b (fromNat m)↗ +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m)↗
ihm :
  Ø ⋁
    Sinf_term.subst (fromNat n) b (fromNat m↗) +ₛ fromNat m↗ =ₛ fromNat m↗ +ₛ Sinf_term.subst (fromNat n) b (fromNat m↗)
⊢ Ø ⋁
    Sinf_term.subst (fromNat n) b (fromNat m↗)↗ +ₛ fromNat m↗ =ₛ
      fromNat m↗ +ₛ Sinf_term.subst (fromNat n) b (fromNat m↗)↗
Tactic:
case a.succ.succ n m ihn ihm =>
  sorry
State after:
no goals

State before:
a b : String
nab : ¬a = b
⊢ Ø ⋁ O +ₛ O =ₛ O +ₛ O
Tactic:
constructor <;> constructor <;> constructor
State after:
no goals

State before:
a b : String
nab : ¬a = b
n : ℕ
ih : Ø ⋁ O +ₛ fromNat n =ₛ fromNat n +ₛ O
⊢ Ø ⋁ O +ₛ fromNat n↗ =ₛ fromNat n↗ +ₛ O
Tactic:
rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
State after:
case S_axiom.plus.plus
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ Ø ⋁ O +ₛ fromNat n↗ =ₛ fromNat n↗ +ₛ O

State before:
case S_axiom.plus.plus
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ Ø ⋁ O +ₛ fromNat n↗ =ₛ fromNat n↗ +ₛ O
Tactic:
constructor <;> try constructor <;> try constructor <;> try assumption
State after:
case S_axiom.plus.plus.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n↗) (NoVars.plus NoVars.O (NoVars.S a✝¹))) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n↗ +ₛ O) (NoVars.plus (NoVars.S a✝¹) NoVars.O))

State before:
case S_axiom.plus.plus.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n↗) (NoVars.plus NoVars.O (NoVars.S a✝¹))) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n↗ +ₛ O) (NoVars.plus (NoVars.S a✝¹) NoVars.O))
Tactic:
simp at *
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ NoVars (fromNat n↗ +ₛ O)
Tactic:
constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ NoVars O
Tactic:
constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂.a.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars O
a✝² a✝¹ : NoVars (fromNat n)
a✝ : NoVars O
e :
  Sinf_const.eval (Sinf_const.coerce (O +ₛ fromNat n) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (fromNat n +ₛ O) (NoVars.plus a✝¹ a✝))
⊢ NoVars (fromNat n)
Tactic:
assumption
State after:
no goals

State before:
a b : String
nab : ¬a = b
n : ℕ
ih : Ø ⋁ Sinf_term.subst (fromNat n) b O +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗
Tactic:
rcases ih with ⟨⟨⟩, ⟨⟩, e⟩
State after:
case S_axiom.plus.plus
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗

State before:
case S_axiom.plus.plus
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ Ø ⋁ Sinf_term.subst (fromNat n) b O↗ +ₛ O =ₛ O +ₛ Sinf_term.subst (fromNat n) b O↗
Tactic:
constructor <;> try constructor <;> try constructor <;> try assumption
State after:
case S_axiom.plus.plus.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O↗ +ₛ O) (NoVars.plus (NoVars.S a✝) NoVars.O)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O↗) (NoVars.plus NoVars.O (NoVars.S a✝)))

State before:
case S_axiom.plus.plus.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O↗ +ₛ O) (NoVars.plus (NoVars.S a✝) NoVars.O)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O↗) (NoVars.plus NoVars.O (NoVars.S a✝)))
Tactic:
simp at *
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ NoVars (O +ₛ Sinf_term.subst (fromNat n) b O↗)
Tactic:
constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ NoVars (Sinf_term.subst (fromNat n) b O↗)
Tactic:
constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.plus.plus.nv₂.a.a
a b : String
nab : ¬a = b
n : ℕ
a✝³ : NoVars (Sinf_term.subst (fromNat n) b O)
a✝² a✝¹ : NoVars O
a✝ : NoVars (Sinf_term.subst (fromNat n) b O)
e :
  Sinf_const.eval (Sinf_const.coerce (Sinf_term.subst (fromNat n) b O +ₛ O) (NoVars.plus a✝³ a✝²)) =
    Sinf_const.eval (Sinf_const.coerce (O +ₛ Sinf_term.subst (fromNat n) b O) (NoVars.plus a✝¹ a✝))
⊢ NoVars (Sinf_term.subst (fromNat n) b O)
Tactic:
assumption
State after:
no goals

State before:
a b : String
nab : ¬a = b
n m : ℕ
ihn :
  Ø ⋁ Sinf_term.subst (fromNat n) b (fromNat m) +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m) →
    Ø ⋁
      Sinf_term.subst (fromNat n) b (fromNat m)↗ +ₛ fromNat m =ₛ fromNat m +ₛ Sinf_term.subst (fromNat n) b (fromNat m)↗
ihm :
  Ø ⋁
    Sinf_term.subst (fromNat n) b (fromNat m↗) +ₛ fromNat m↗ =ₛ fromNat m↗ +ₛ Sinf_term.subst (fromNat n) b (fromNat m↗)
⊢ Ø ⋁
    Sinf_term.subst (fromNat n) b (fromNat m↗)↗ +ₛ fromNat m↗ =ₛ
      fromNat m↗ +ₛ Sinf_term.subst (fromNat n) b (fromNat m↗)↗
Tactic:
sorry
State after:
no goals

State before:
a b : String
n : ℕ
ab : a = b
⊢ Ø ⋁
    match isTrue ab with
    | isTrue h => ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
    | isFalse h =>
      ∀ₛ b ;
        ((match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a) +ₛ
            match isTrue ab with
            | isTrue h => fromNat n
            | isFalse h => _ b) =ₛ
          (match isTrue ab with
            | isTrue h => fromNat n
            | isFalse h => _ b) +ₛ
            match String.decEq a a with
            | isTrue h => fromNat n
            | isFalse h => _ a
Tactic:
simp
State after:
a b : String
n : ℕ
ab : a = b
⊢ Ø ⋁ ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a

State before:
a b : String
n : ℕ
ab : a = b
⊢ Ø ⋁ ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
Tactic:
rw [ab]
State after:
a b : String
n : ℕ
ab : a = b
⊢ Ø ⋁ ∀ₛ b ; _ b +ₛ _ b =ₛ _ b +ₛ _ b

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

State before:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ), Ø ⋁ _ b +ₛ _ b =ₛ _ b +ₛ _ b [b ≔ fromNat n]
Tactic:
simp
State after:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ),
    Ø ⋁
      ((match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) =ₛ
        (match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b

State before:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ),
    Ø ⋁
      ((match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) =ₛ
        (match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match String.decEq b b with
          | isTrue h => fromNat n
          | isFalse h => _ b
Tactic:
rw [String.decEq_refl b]
State after:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ),
    Ø ⋁
      ((match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) =ₛ
        (match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b

State before:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ),
    Ø ⋁
      ((match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) =ₛ
        (match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b) +ₛ
          match isTrue (_ : b = b) with
          | isTrue h => fromNat n
          | isFalse h => _ b
Tactic:
simp
State after:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ), Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n

State before:
case a
a b : String
n : ℕ
ab : a = b
⊢ ∀ (n : ℕ), Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n
Tactic:
intros n
State after:
case a
a b : String
n✝ : ℕ
ab : a = b
n : ℕ
⊢ Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n

State before:
case a
a b : String
n✝ : ℕ
ab : a = b
n : ℕ
⊢ Ø ⋁ fromNat n +ₛ fromNat n =ₛ fromNat n +ₛ fromNat n
Tactic:
constructor <;> constructor <;> apply NoVars.fromNat
State after:
no goals