internlm/Lean-Github huggingface dataset:
Theorem: Sinf.succ_cong
Proof state before:
case nv₂
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
⊢ NoVars (θ₂↗)
Tactic:
constructor <;> try assumption
Proof state after:
no goals
Theorem: Sinf.succ_cong
Proof state before:
case nv₂.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
⊢ NoVars θ₂
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.succ_cong
Proof state before:
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁↗ =ₛ θ₂↗
Tactic:
exact (S_weakening (θ₁↗ =ₛ θ₂↗) ne)
Proof state after:
no goals
Theorem: Sinf.succ_inj
Proof state before:
⊢ ∀ {θ₁ θ₂ : Sinf_term} {Δ : Ctx Sinf}, Δ ⋁ θ₁↗ =ₛ θ₂↗ → Δ ⋁ θ₁ =ₛ θ₂
Tactic:
intros θ₁ θ₂ Δ _12
Proof state after:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁↗ =ₛ θ₂↗
⊢ Δ ⋁ θ₁ =ₛ θ₂
Theorem: Sinf.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁↗ =ₛ θ₂↗
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases _12
Proof state after:
case S_axiom
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁✝ : NoVars (θ₁↗)
nv₂✝ : NoVars (θ₂↗)
a✝ : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁✝) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂✝)
⊢ Δ ⋁ θ₁ =ₛ θ₂

case S_weakening
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂
Theorem: Sinf.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars (θ₁↗)
nv₂ : NoVars (θ₂↗)
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
case S_axiom nv₁ nv₂ e =>
  cases nv₁; cases nv₂; constructor <;> try assumption
  simp at e
  assumption
Proof state after:
no goals
Theorem: Sinf.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂
Tactic:
case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₂) ne)
Proof state after:
no goals
Theorem: Sinf.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars (θ₁↗)
nv₂ : NoVars (θ₂↗)
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases nv₁
Proof state after:
case S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₂ : NoVars (θ₂↗)
a✝ : NoVars θ₁
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Theorem: Sinf.succ_inj
Proof state before:
case S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₂ : NoVars (θ₂↗)
a✝ : NoVars θ₁
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases nv₂
Proof state after:
case S.S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Δ ⋁ θ₁ =ₛ θ₂
Theorem: Sinf.succ_inj
Proof state before:
case S.S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
constructor <;> try assumption
Proof state after:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Theorem: Sinf.succ_inj
Proof state before:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Tactic:
simp at e
Proof state after:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Theorem: Sinf.succ_inj
Proof state before:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.succ_inj
Proof state before:
case S.S.nv₂
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ NoVars θ₂
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂
Tactic:
exact (S_weakening (θ₁ =ₛ θ₂) ne)
Proof state after:
no goals
Theorem: Sinf.consistent
Proof state before:
⊢ ∃ α, ¬(Ø ⋁ α)
Tactic:
exists (¬ₛ O =ₛ O)
Proof state after:
⊢ ¬(Ø ⋁ ¬ₛ O =ₛ O)
Theorem: Sinf.consistent
Proof state before:
⊢ ¬(Ø ⋁ ¬ₛ O =ₛ O)
Tactic:
intros p
Proof state after:
p : Ø ⋁ ¬ₛ O =ₛ O
⊢ False
Theorem: Sinf.consistent
Proof state before:
p : Ø ⋁ ¬ₛ O =ₛ O
⊢ False
Tactic:
cases p
Proof state after:
case S_axiom_neg
nv₁✝ nv₂✝ : NoVars O
a✝ : Sinf_const.eval (Sinf_const.coerce O nv₁✝) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂✝)
⊢ False
Theorem: Sinf.consistent
Proof state before:
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₁) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
Tactic:
case S_axiom_neg nv₁ nv₂ p =>
  rw [NoVars.unique nv₁ nv₂] at p
  exact p rfl
Proof state after:
no goals
Theorem: Sinf.consistent
Proof state before:
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₁) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
Tactic:
rw [NoVars.unique nv₁ nv₂] at p
Proof state after:
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₂) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
Theorem: Sinf.consistent
Proof state before:
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₂) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
Tactic:
exact p rfl
Proof state after:
no goals
Theorem: Sinf.contradiction_yields_anything
Proof state before:
⊢ ∀ {α β : Sinf} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α) → Δ ⋁ β
Tactic:
intros α β Δ contr
Proof state after:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
have iβ := S_inr β contr
Proof state after:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
have s_return := S_in iβ
Proof state after:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
cases S_de_morgan_inv s_return
Proof state after:
case intro
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
left✝ : β :: Δ ⋁ ¬ₛ α
right✝ : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β
Tactic:
apply S_contraction
Proof state after:
case a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ β
Tactic:
apply S_section (¬ₛ α)
Proof state after:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ ¬ₛ α

case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ ¬ₛ ¬ₛ α ∨ₛ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ ¬ₛ α
Tactic:
apply S_out
Proof state after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ α
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ α
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ ¬ₛ ¬ₛ α ∨ₛ β
Tactic:
apply S_out
Proof state after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ (¬ₛ ¬ₛ α) :: Δ ⋁ β
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ (¬ₛ ¬ₛ α) :: Δ ⋁ β
Tactic:
apply S_exchange_ctx
Proof state after:
case a.a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ ¬ₛ α
Theorem: Sinf.contradiction_yields_anything
Proof state before:
case a.a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ ¬ₛ α
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.var_refl
Proof state before:
a : String
⊢ Ø ⋁ ∀ₛ a ; _ a =ₛ _ a
Tactic:
apply S_induction
Proof state after:
case a
a : String
⊢ ∀ (n : ℕ), Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Theorem: Sinf.var_refl
Proof state before:
case a
a : String
⊢ ∀ (n : ℕ), Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Tactic:
intros n
Proof state after:
case a
a : String
n : ℕ
⊢ Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Theorem: Sinf.var_refl
Proof state before:
case a
a : String
n : ℕ
⊢ Ø ⋁ _ a =ₛ _ a [a ≔ fromNat n]
Tactic:
constructor <;> simp <;> try rw [String.decEq_refl a] <;> apply NoVars.fromNat
Proof 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)))
Theorem: Sinf.var_refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.var_refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof state before:
θ : Sinf_term
nv : NoVars θ
⊢ Ø ⋁ θ =ₛ θ
Tactic:
induction nv
Proof 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✝ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Theorem: Sinf.refl
Proof state before:
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O
Tactic:
case O => constructor <;> try constructor
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof state before:
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O
Tactic:
constructor <;> try constructor
Proof state after:
no goals
Theorem: Sinf.refl
Proof state before:
case nv₂
θ : Sinf_term
⊢ NoVars O
Tactic:
constructor
Proof state after:
no goals
Theorem: Sinf.refl
Proof state before:
θ t✝ : Sinf_term
a✝ : NoVars t✝
nv : Ø ⋁ t✝ =ₛ t✝
⊢ Ø ⋁ t✝↗ =ₛ t✝↗
Tactic:
rcases nv with ⟨nv₁, nv₂, e⟩
Proof 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✝↗
Theorem: Sinf.refl
Proof 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
Proof 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✝
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof 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✝
Theorem: Sinf.refl
Proof state before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Tactic:
rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
Proof 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₁₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Theorem: Sinf.refl
Proof 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₂⟩
Proof 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₂₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof state before:
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Tactic:
rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
Proof 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₁₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Theorem: Sinf.refl
Proof 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₂⟩
Proof 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₂₂)
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.refl
Proof 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
Proof state after:
no goals
Theorem: Sinf.plus_comm
Proof state before:
a b : String
⊢ Ø ⋁ ∀ₛ a ; ∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a
Tactic:
apply S_induction
Proof state after:
case a
a b : String
⊢ ∀ (n : ℕ), Ø ⋁ (∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a) [a ≔ fromNat n]
Theorem: Sinf.plus_comm
Proof state before:
case a
a b : String
⊢ ∀ (n : ℕ), Ø ⋁ (∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a) [a ≔ fromNat n]
Tactic:
intros n
Proof state after:
case a
a b : String
n : ℕ
⊢ Ø ⋁ (∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a) [a ≔ fromNat n]
Theorem: Sinf.plus_comm
Proof state before:
case a
a b : String
n : ℕ
⊢ Ø ⋁ (∀ₛ b ; _ a +ₛ _ b =ₛ _ b +ₛ _ a) [a ≔ fromNat n]
Tactic:
simp
Proof 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