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

State before:
⊢ ∀ {θ₁ : Sinf_term} (θ₂ : Sinf_term) {θ₃ : Sinf_term} {Δ : Ctx Sinf}, Δ ⋁ θ₁ =ₛ θ₂ → Δ ⋁ θ₂ =ₛ θ₃ → Δ ⋁ θ₁ =ₛ θ₃
Tactic:
intros θ₁ θ₂ θ₃ Δ _12 _23
State after:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
_23 : Δ ⋁ θ₂ =ₛ θ₃
⊢ Δ ⋁ θ₁ =ₛ θ₃

State before:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
_23 : Δ ⋁ θ₂ =ₛ θ₃
⊢ Δ ⋁ θ₁ =ₛ θ₃
Tactic:
cases _12
State after:
case S_axiom
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_23 : Δ ⋁ θ₂ =ₛ θ₃
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✝ : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃

State before:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_23 : Δ ⋁ θ₂ =ₛ θ₃
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 _23
  case S_axiom nv₂' nv₃ e' =>
    constructor <;> try assumption
    rw [NoVars.unique nv₂ nv₂'] at e
    exact (Eq.trans e e')
  case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₃) ne)
State after:
no goals

State before:
θ₁ θ₂ θ₃ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₃) ne)
State after:
no goals

State before:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_23 : Δ ⋁ θ₂ =ₛ θ₃
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₃
Tactic:
cases _23
State after:
case S_axiom
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
nv₁✝ : NoVars θ₂
nv₂✝ : NoVars θ₃
a✝ : Sinf_const.eval (Sinf_const.coerce θ₂ nv₁✝) = Sinf_const.eval (Sinf_const.coerce θ₃ nv₂✝)
⊢ Δ ⋁ θ₁ =ₛ θ₃

case S_weakening
θ₁ θ₂ θ₃ : Sinf_term
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃

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₂)
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' =>
  constructor <;> try assumption
  rw [NoVars.unique nv₂ nv₂'] at e
  exact (Eq.trans e e')
State after:
no goals

State before:
θ₁ θ₂ θ₃ : Sinf_term
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₃) ne)
State after:
no goals

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₂)
nv₂' : NoVars θ₂
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Δ ⋁ θ₁ =ₛ θ₃
Tactic:
constructor <;> try assumption
State after:
case a
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
nv₂' : NoVars θ₂
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)

State before:
case a
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
nv₂' : NoVars θ₂
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
Tactic:
rw [NoVars.unique nv₂ nv₂'] at e
State after:
case a
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ nv₂' : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂')
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)

State before:
case a
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ nv₂' : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂')
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
Tactic:
exact (Eq.trans e e')
State after:
no goals

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₂)
nv₂' : NoVars θ₂
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
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
exact (S_weakening (θ₁ =ₛ θ₃) ne)
State after:
no goals

State before:
θ₁ θ₂ θ₃ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
exact (S_weakening (θ₁ =ₛ θ₃) ne)
State after:
no goals