Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺⟨s⟩ Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
cases h
State after:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Δ₁ ⊆ Δ₂

case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂

State before:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Δ₁ ⊆ Δ₂

case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
{ exact Redux.antimonotone (by assumption) }
State after:
case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂

State before:
case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
{ exact List.Subset.refl Δ₂ }
State after:
no goals

State before:
case redux
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
exact Redux.antimonotone (by assumption)
State after:
no goals

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Redux ?m.13639 ?m.13640 Δ₂ Δ₁
Tactic:
assumption
State after:
no goals

State before:
case refl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
exact List.Subset.refl Δ₂
State after:
no goals