internlm/Lean-Github huggingface dataset:
Theorem: HasDerivAt.matrix_inv
Proof state before:
case h.e'_10
ι : Type ?u.34796
R : Type u_3
A : Type u_2
m : Type u_1
n : Type ?u.34808
p : Type ?u.34811
q : Type ?u.34814
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : NontriviallyNormedField R
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra R A
inst✝ : CompleteSpace A
X : R → Matrix m m A
X' : Matrix m m A
r : R
hX : HasFDerivAt X (ContinuousLinearMap.smulRight 1 X') r
u : (Matrix m m A)ˣ
hu : ↑u = X r
this :
  HasFDerivAt Ring.inverse
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r))) (Ring.inverse (X r))) (X r)
⊢ ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r) * X' * Ring.inverse (X r)) =
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r))) (Ring.inverse (X r))).comp
      (ContinuousLinearMap.smulRight 1 X')
Tactic:
ext r : 2
Proof state after:
case h.e'_10.h.a
ι : Type ?u.34796
R : Type u_3
A : Type u_2
m : Type u_1
n : Type ?u.34808
p : Type ?u.34811
q : Type ?u.34814
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : NontriviallyNormedField R
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra R A
inst✝ : CompleteSpace A
X : R → Matrix m m A
X' : Matrix m m A
r✝ : R
hX : HasFDerivAt X (ContinuousLinearMap.smulRight 1 X') r✝
u : (Matrix m m A)ˣ
hu : ↑u = X r✝
this :
  HasFDerivAt Ring.inverse
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r✝))) (Ring.inverse (X r✝))) (X r✝)
r j✝ : m
⊢ (ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r✝) * X' * Ring.inverse (X r✝))) 1 r j✝ =
    ((-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r✝))) (Ring.inverse (X r✝))).comp
        (ContinuousLinearMap.smulRight 1 X'))
      1 r j✝
Theorem: HasDerivAt.matrix_inv
Proof state before:
case h.e'_10.h.a
ι : Type ?u.34796
R : Type u_3
A : Type u_2
m : Type u_1
n : Type ?u.34808
p : Type ?u.34811
q : Type ?u.34814
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : NontriviallyNormedField R
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra R A
inst✝ : CompleteSpace A
X : R → Matrix m m A
X' : Matrix m m A
r✝ : R
hX : HasFDerivAt X (ContinuousLinearMap.smulRight 1 X') r✝
u : (Matrix m m A)ˣ
hu : ↑u = X r✝
this :
  HasFDerivAt Ring.inverse
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r✝))) (Ring.inverse (X r✝))) (X r✝)
r j✝ : m
⊢ (ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r✝) * X' * Ring.inverse (X r✝))) 1 r j✝ =
    ((-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r✝))) (Ring.inverse (X r✝))).comp
        (ContinuousLinearMap.smulRight 1 X'))
      1 r j✝
Tactic:
simp [Matrix.mul_smul, (ContinuousLinearMap.smulRight_apply), (ContinuousLinearMap.comp_apply), (ContinuousLinearMap.neg_apply)]
Proof state after:
no goals
Theorem: Sinf_term.succ_inj
Proof state before:
θ₁ θ₂ : Sinf_term
⊢ θ₁↗ = θ₂↗ → θ₁ = θ₂
Tactic:
induction θ₁ <;> induction θ₂ <;> simp at *
Proof state after:
no goals
Theorem: S_exchange
Proof state before:
⊢ ∀ {α β : Sinf} {Δ : Ctx Sinf}, Δ ⋁ α ∨ₛ β → Δ ⋁ β ∨ₛ α
Tactic:
intros α β Δ αβ
Proof state after:
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ β ∨ₛ α
Theorem: S_exchange
Proof state before:
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ β ∨ₛ α
Tactic:
apply S_out
Proof state after:
case a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ β :: Δ ⋁ α
Theorem: S_exchange
Proof state before:
case a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ β :: Δ ⋁ α
Tactic:
apply S_exchange_ctx
Proof state after:
case a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ α :: Δ ⋁ β
Theorem: S_exchange
Proof state before:
case a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ α :: Δ ⋁ β
Tactic:
apply S_in
Proof state after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ α ∨ₛ β
Theorem: S_exchange
Proof state before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ α ∨ₛ β
Tactic:
assumption
Proof state after:
no goals
Theorem: S_assoc
Proof state before:
⊢ ∀ {α β γ : Sinf} {Δ : Ctx Sinf}, Δ ⋁ α ∨ₛ β ∨ₛ γ ↔ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
intros α β γ Δ
Proof state after:
α β γ : Sinf
Δ : Ctx Sinf
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ ↔ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Theorem: S_assoc
Proof state before:
α β γ : Sinf
Δ : Ctx Sinf
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ ↔ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
constructor <;> intros h
Proof state after:
case mp
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)

case mpr
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Theorem: S_assoc
Proof state before:
case mp
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
apply S_out
Proof state after:
case mp.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ α :: Δ ⋁ β ∨ₛ γ
Theorem: S_assoc
Proof state before:
case mp.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ α :: Δ ⋁ β ∨ₛ γ
Tactic:
apply S_out
Proof state after:
case mp.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ β :: α :: Δ ⋁ γ
Theorem: S_assoc
Proof state before:
case mp.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ β :: α :: Δ ⋁ γ
Tactic:
apply S_split
Proof state after:
case mp.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Theorem: S_assoc
Proof state before:
case mp.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Tactic:
apply S_in
Proof state after:
case mp.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Theorem: S_assoc
Proof state before:
case mp.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Tactic:
assumption
Proof state after:
no goals
Theorem: S_assoc
Proof state before:
case mpr
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Tactic:
apply S_out
Proof state after:
case mpr.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Theorem: S_assoc
Proof state before:
case mpr.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Tactic:
apply S_join
Proof state after:
case mpr.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ β :: α :: Δ ⋁ γ
Theorem: S_assoc
Proof state before:
case mpr.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ β :: α :: Δ ⋁ γ
Tactic:
apply S_in
Proof state after:
case mpr.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ α :: Δ ⋁ β ∨ₛ γ
Theorem: S_assoc
Proof state before:
case mpr.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ α :: Δ ⋁ β ∨ₛ γ
Tactic:
apply S_in
Proof state after:
case mpr.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Theorem: S_assoc
Proof state before:
case mpr.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
assumption
Proof state after:
no goals
Theorem: S_contraction
Proof state before:
⊢ ∀ {α : Sinf} {Δ : Ctx Sinf}, Δ ⋁ α ∨ₛ α → Δ ⋁ α
Tactic:
intros α Δ αα
Proof state after:
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ Δ ⋁ α
Theorem: S_contraction
Proof state before:
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ Δ ⋁ α
Tactic:
apply S_contraction_ctx
Proof state after:
case a
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ α :: Δ ⋁ α
Theorem: S_contraction
Proof state before:
case a
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ α :: Δ ⋁ α
Tactic:
apply S_in
Proof state after:
case a.a
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ Δ ⋁ α ∨ₛ α
Theorem: S_contraction
Proof state before:
case a.a
α : Sinf
Δ : Ctx Sinf
αα : Δ ⋁ α ∨ₛ α
⊢ Δ ⋁ α ∨ₛ α
Tactic:
assumption
Proof state after:
no goals
Theorem: S_inr
Proof state before:
⊢ ∀ (α : Sinf) {β : Sinf} {Δ : Ctx Sinf}, Δ ⋁ β → Δ ⋁ α ∨ₛ β
Tactic:
intros α β Δ b
Proof state after:
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ α ∨ₛ β
Theorem: S_inr
Proof state before:
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ α ∨ₛ β
Tactic:
apply S_exchange
Proof state after:
case a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ β ∨ₛ α
Theorem: S_inr
Proof state before:
case a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ β ∨ₛ α
Tactic:
apply S_out
Proof state after:
case a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ β :: Δ ⋁ α
Theorem: S_inr
Proof state before:
case a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ β :: Δ ⋁ α
Tactic:
apply S_weakening
Proof state after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ β
Theorem: S_inr
Proof state before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ β
Tactic:
assumption
Proof state after:
no goals
Theorem: S_inl
Proof state before:
⊢ ∀ {α : Sinf} (β : Sinf) {Δ : Ctx Sinf}, Δ ⋁ α → Δ ⋁ α ∨ₛ β
Tactic:
intros α β Δ a
Proof state after:
α β : Sinf
Δ : Ctx Sinf
a : Δ ⋁ α
⊢ Δ ⋁ α ∨ₛ β
Theorem: S_inl
Proof state before:
α β : Sinf
Δ : Ctx Sinf
a : Δ ⋁ α
⊢ Δ ⋁ α ∨ₛ β
Tactic:
apply S_exchange
Proof state after:
case a
α β : Sinf
Δ : Ctx Sinf
a : Δ ⋁ α
⊢ Δ ⋁ β ∨ₛ α
Theorem: S_inl
Proof state before:
case a
α β : Sinf
Δ : Ctx Sinf
a : Δ ⋁ α
⊢ Δ ⋁ β ∨ₛ α
Tactic:
exact (S_inr β a)
Proof state after:
no goals
Theorem: S_dne
Proof state before:
⊢ ∀ {α : Sinf} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ ¬ₛ α → Δ ⋁ α
Tactic:
intros α Δ dn
Proof state after:
α : Sinf
Δ : Ctx Sinf
dn : Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ α
Theorem: S_dne
Proof state before:
α : Sinf
Δ : Ctx Sinf
dn : Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ α
Tactic:
cases dn
Proof state after:
case S_weakening
α δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α

case S_dni
α : Sinf
Δ : Ctx Sinf
a✝ : Δ ⋁ α
⊢ Δ ⋁ α
Theorem: S_dne
Proof state before:
α δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α
Tactic:
case S_weakening ne => exact (S_weakening α ne)
Proof state after:
no goals
Theorem: S_dne
Proof state before:
α : Sinf
Δ : Ctx Sinf
β : Δ ⋁ α
⊢ Δ ⋁ α
Tactic:
case S_dni β => exact β
Proof state after:
no goals
Theorem: S_dne
Proof state before:
α δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α
Tactic:
exact (S_weakening α ne)
Proof state after:
no goals
Theorem: S_dne
Proof state before:
α : Sinf
Δ : Ctx Sinf
β : Δ ⋁ α
⊢ Δ ⋁ α
Tactic:
exact β
Proof state after:
no goals
Theorem: S_de_morgan_inv
Proof state before:
⊢ ∀ {α β : Sinf} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ (α ∨ₛ β) → (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
intros α β Δ d
Proof state after:
α β : Sinf
Δ : Ctx Sinf
d : Δ ⋁ ¬ₛ (α ∨ₛ β)
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Theorem: S_de_morgan_inv
Proof state before:
α β : Sinf
Δ : Ctx Sinf
d : Δ ⋁ ¬ₛ (α ∨ₛ β)
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
cases d
Proof state after:
case S_weakening
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)

case S_de_morgan
α β : Sinf
Δ : Ctx Sinf
a✝¹ : Δ ⋁ ¬ₛ α
a✝ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Theorem: S_de_morgan_inv
Proof state before:
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)
Tactic:
case S_weakening ne => exact And.intro (S_weakening (¬ₛ α) ne) (S_weakening (¬ₛ β) ne)
Proof state after:
no goals
Theorem: S_de_morgan_inv
Proof state before:
α β : Sinf
Δ : Ctx Sinf
nα : Δ ⋁ ¬ₛ α
nβ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
case S_de_morgan nα nβ => exact And.intro nα nβ
Proof state after:
no goals
Theorem: S_de_morgan_inv
Proof state before:
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)
Tactic:
exact And.intro (S_weakening (¬ₛ α) ne) (S_weakening (¬ₛ β) ne)
Proof state after:
no goals
Theorem: S_de_morgan_inv
Proof state before:
α β : Sinf
Δ : Ctx Sinf
nα : Δ ⋁ ¬ₛ α
nβ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
exact And.intro nα nβ
Proof state after:
no goals
Theorem: S_neg_forall_inv
Proof state before:
⊢ ∀ {α : Sinf} {x : String} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ (∀ₛ x ; α) → ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
intros α x Δ nf
Proof state after:
α : Sinf
x : String
Δ : Ctx Sinf
nf : Δ ⋁ ¬ₛ (∀ₛ x ; α)
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
nf : Δ ⋁ ¬ₛ (∀ₛ x ; α)
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
cases nf
Proof state after:
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]

case S_neg_forall
α : Sinf
x : String
Δ : Ctx Sinf
θ✝ : Sinf_term
a✝ : Δ ⋁ ¬ₛ α [x ≔ θ✝]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
case S_weakening ne => exists (_ x); exact (S_weakening (¬ₛ α[x ≔ _ x]) ne)
Proof state after:
no goals
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
θ : Sinf_term
β : Δ ⋁ ¬ₛ α [x ≔ θ]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
case S_neg_forall θ β => exists θ
Proof state after:
no goals
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
exists (_ x)
Proof state after:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ _ x]
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ _ x]
Tactic:
exact (S_weakening (¬ₛ α[x ≔ _ x]) ne)
Proof state after:
no goals
Theorem: S_neg_forall_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
θ : Sinf_term
β : Δ ⋁ ¬ₛ α [x ≔ θ]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
exists θ
Proof state after:
no goals
Theorem: S_induction_inv
Proof state before:
⊢ ∀ {α : Sinf} {x : String} {Δ : Ctx Sinf}, Δ ⋁ ∀ₛ x ; α → ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
intros α x Δ f
Proof state after:
α : Sinf
x : String
Δ : Ctx Sinf
f : Δ ⋁ ∀ₛ x ; α
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
f : Δ ⋁ ∀ₛ x ; α
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
cases f
Proof state after:
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]

case S_induction
α : Sinf
x : String
Δ : Ctx Sinf
a✝ : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
case S_weakening ne => intros n; exact (S_weakening (α [x ≔ n]) ne)
Proof state after:
no goals
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
i : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
case S_induction i => assumption
Proof state after:
no goals
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
intros n
Proof state after:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
n : ℕ
⊢ δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
n : ℕ
⊢ δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
exact (S_weakening (α [x ≔ n]) ne)
Proof state after:
no goals
Theorem: S_induction_inv
Proof state before:
α : Sinf
x : String
Δ : Ctx Sinf
i : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
assumption
Proof state after:
no goals
Theorem: Sinf.eq_trans
Proof state before:
⊢ ∀ {θ₁ : Sinf_term} (θ₂ : Sinf_term) {θ₃ : Sinf_term} {Δ : Ctx Sinf}, Δ ⋁ θ₁ =ₛ θ₂ → Δ ⋁ θ₂ =ₛ θ₃ → Δ ⋁ θ₁ =ₛ θ₃
Tactic:
intros θ₁ θ₂ θ₃ Δ _12 _23
Proof state after:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
_23 : Δ ⋁ θ₂ =ₛ θ₃
⊢ Δ ⋁ θ₁ =ₛ θ₃
Theorem: Sinf.eq_trans
Proof state before:
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
_23 : Δ ⋁ θ₂ =ₛ θ₃
⊢ Δ ⋁ θ₁ =ₛ θ₃
Tactic:
cases _12
Proof 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 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Theorem: Sinf.eq_trans
Proof 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)
Proof state after:
no goals
Theorem: Sinf.eq_trans
Proof state before:
θ₁ θ₂ θ₃ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₃) ne)
Proof state after:
no goals
Theorem: Sinf.eq_trans
Proof 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
Proof 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✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Theorem: Sinf.eq_trans
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₂)
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')
Proof state after:
no goals
Theorem: Sinf.eq_trans
Proof 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)
Proof state after:
no goals
Theorem: Sinf.eq_trans
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₂)
nv₂' : NoVars θ₂
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Δ ⋁ θ₁ =ₛ θ₃
Tactic:
constructor <;> try assumption
Proof 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₃)
Theorem: Sinf.eq_trans
Proof 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
Proof 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₃)
Theorem: Sinf.eq_trans
Proof 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')
Proof state after:
no goals
Theorem: Sinf.eq_trans
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₂)
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.eq_trans
Proof 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)
Proof state after:
no goals
Theorem: Sinf.eq_trans
Proof state before:
θ₁ θ₂ θ₃ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
_23 : δ✝ :: Δ✝ ⋁ θ₂ =ₛ θ₃
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₃
Tactic:
exact (S_weakening (θ₁ =ₛ θ₃) ne)
Proof state after:
no goals
Theorem: Sinf.succ_cong
Proof state before:
⊢ ∀ {θ₁ θ₂ : Sinf_term} {Δ : Ctx Sinf}, Δ ⋁ θ₁ =ₛ θ₂ → Δ ⋁ θ₁↗ =ₛ θ₂↗
Tactic:
intros θ₁ θ₂ Δ _12
Proof state after:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁ =ₛ θ₂
⊢ Δ ⋁ θ₁↗ =ₛ θ₂↗
Theorem: Sinf.succ_cong
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_cong
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 =>
  constructor <;> try constructor <;> try assumption
  simp at *
  assumption
Proof state after:
no goals
Theorem: Sinf.succ_cong
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_cong
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:
constructor <;> try constructor <;> try assumption
Proof 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₂)
⊢ Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S nv₁)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S nv₂))
Theorem: Sinf.succ_cong
Proof 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₂)
⊢ Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S nv₁)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S nv₂))
Tactic:
simp at *
Proof 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₂)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
Theorem: Sinf.succ_cong
Proof 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₂)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
Tactic:
assumption
Proof state after:
no goals