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

State before:
⊢ ∃ α, ¬(Ø ⋁ α)
Tactic:
exists (¬ₛ O =ₛ O)
State after:
⊢ ¬(Ø ⋁ ¬ₛ O =ₛ O)

State before:
⊢ ¬(Ø ⋁ ¬ₛ O =ₛ O)
Tactic:
intros p
State after:
p : Ø ⋁ ¬ₛ O =ₛ O
⊢ False

State before:
p : Ø ⋁ ¬ₛ O =ₛ O
⊢ False
Tactic:
cases p
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

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
State after:
no goals

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
State after:
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₂) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False

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
State after:
no goals