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

State before:
θ : Sinf_term
nv : NoVars θ
⊢ Ø ⋁ θ =ₛ θ
Tactic:
induction nv
State after:
case O
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O

case S
θ t✝ : Sinf_term
a✝ : NoVars t✝
a_ih✝ : Ø ⋁ t✝ =ₛ t✝
⊢ Ø ⋁ t✝↗ =ₛ t✝↗

case plus
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
a_ih✝¹ : Ø ⋁ θ₁✝ =ₛ θ₁✝
a_ih✝ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝

case times
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
a_ih✝¹ : Ø ⋁ θ₁✝ =ₛ θ₁✝
a_ih✝ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝

State before:
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O
Tactic:
case O => constructor <;> try constructor
State after:
no goals

State before:
θ t✝ : Sinf_term
a✝ : NoVars t✝
nv : Ø ⋁ t✝ =ₛ t✝
⊢ Ø ⋁ t✝↗ =ₛ t✝↗
Tactic:
case S nv =>
  rcases nv with ⟨nv₁, nv₂, e⟩
  constructor <;> try constructor
  assumption
State after:
no goals

State before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Tactic:
case plus nv₁ nv₂ =>
  rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
  rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
  constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Tactic:
case times nv₁ nv₂ =>
  rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
  rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
  constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O
Tactic:
constructor <;> try constructor
State after:
no goals

State before:
case nv₂
θ : Sinf_term
⊢ NoVars O
Tactic:
constructor
State after:
no goals

State before:
θ t✝ : Sinf_term
a✝ : NoVars t✝
nv : Ø ⋁ t✝ =ₛ t✝
⊢ Ø ⋁ t✝↗ =ₛ t✝↗
Tactic:
rcases nv with ⟨nv₁, nv₂, e⟩
State after:
case S_axiom
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ Ø ⋁ t✝↗ =ₛ t✝↗

State before:
case S_axiom
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ Ø ⋁ t✝↗ =ₛ t✝↗
Tactic:
constructor <;> try constructor
State after:
case S_axiom.nv₂.a
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ NoVars t✝

State before:
case S_axiom.nv₂.a
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ NoVars t✝
Tactic:
assumption
State after:
no goals

State before:
case S_axiom.nv₂
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ NoVars (t✝↗)
Tactic:
constructor
State after:
case S_axiom.nv₂.a
θ t✝ : Sinf_term
a✝ nv₁ nv₂ : NoVars t✝
e : Sinf_const.eval (Sinf_const.coerce t✝ nv₁) = Sinf_const.eval (Sinf_const.coerce t✝ nv₂)
⊢ NoVars t✝

State before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Tactic:
rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
State after:
case S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝

State before:
case S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Tactic:
rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
State after:
case S_axiom.S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝

State before:
case S_axiom.S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Tactic:
constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.S_axiom.nv₂
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ NoVars (θ₁✝ +ₛ θ₂✝)
Tactic:
constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.S_axiom.nv₂.a
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ NoVars θ₂✝
Tactic:
assumption
State after:
no goals

State before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Tactic:
rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
State after:
case S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝

State before:
case S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Tactic:
rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
State after:
case S_axiom.S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝

State before:
case S_axiom.S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Tactic:
constructor <;> try constructor <;> try assumption
State after:
no goals

State before:
case S_axiom.S_axiom.nv₂
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ NoVars (θ₁✝ *ₛ θ₂✝)
Tactic:
constructor <;> try assumption
State after:
no goals