Theorem: Execution.Grouped.Steps.deterministic (ReactorModel/Execution/Theorems/Grouped/Steps.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : Steps s s₁
e₂ : Steps s s₂
n : State.Nontrivial s
ht : s₁.tag = s₂.tag
hp : s₁.progress = s₂.progress
⊢ s₁ = s₂
Tactic:
induction e₁ <;> cases e₂
State after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s₂
ht : s₂.tag = s₂.tag
hp : s₂.progress = s₂.progress
⊢ s₂ = s₂

case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
a✝ : Step s₂ s₂✝
n : State.Nontrivial s₂
⊢ s₃✝ = s₂

case step.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : Step s₁✝ s₂✝¹
a✝² : Steps s₂✝¹ s₃✝
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s₂
ht : s₂.tag = s₂.tag
hp : s₂.progress = s₂.progress
⊢ s₂ = s₂
Tactic:
case refl.refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
case step.step e₁ _ hi _ e₂ e₂' => 
  exact hi (e₁.deterministic e₂ ▸ e₂') (e₁.preserves_nontrivial n) ht hp
State after:
no goals

State before:
case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
a✝ : Step s₂ s₂✝
n : State.Nontrivial s₂
⊢ s₃✝ = s₂
Tactic:
all_goals cases ‹Step _ _›
State after:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s✝ = s₂

case refl.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s✝ ↓ₜ s₂✝
⊢ s✝ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
e' : Steps s₂✝ s₂
e : s✝ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
case refl.step.time e' e   => exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
case step.refl.time e' _ e => exact absurd ht.symm $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s✝ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
all_goals cases ‹Steps _ _›
State after:
case refl.step.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
a✝ : s✝ ↓ᵢ| s₂
⊢ s✝ = s₂

case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₂✝.tag = s₂.tag → s₂✝.progress = s₂.progress → s₂✝ = s₂
ht : s₂✝.tag = s₂.tag
hp : s₂✝.progress = s₂.progress
⊢ s₂✝ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ e' : State α
n : State.Nontrivial e'
ht : e'.tag = s₂.tag
hp : e'.progress = s₂.progress
e : e' ↓ᵢ| s₂
⊢ e' = s₂
Tactic:
case refl.step.inst.refl e' e => exact absurd hp $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₂✝.tag = s₂.tag → s₂✝.progress = s₂.progress → s₂✝ = s₂
ht : s₂✝.tag = s₂.tag
hp : s₂✝.progress = s₂.progress
⊢ s₂✝ = s₂
Tactic:
case step.refl.inst.refl e _  => exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₂
⊢ s✝ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₃✝ = s₂
Tactic:
all_goals cases ‹Step _ _›
State after:
case refl.step.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s✝ = s₂

case refl.step.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₂
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s✝ = s₂

case step.refl.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
case refl.step.inst.step.time e _ f' f => exact absurd ht $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
case step.refl.inst.step.time e _ f' f => exact absurd ht.symm $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s✝ = s₂
Tactic:
case refl.step.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
case step.refl.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s₂
ht : s₂.tag = s₂.tag
hp : s₂.progress = s₂.progress
⊢ s₂ = s₂
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
n : State.Nontrivial s₁✝
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ s₂
⊢ s₃✝ = s₂
Tactic:
exact hi (e₁.deterministic e₂ ▸ e₂') (e₁.preserves_nontrivial n) ht hp
State after:
no goals

State before:
case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
a✝ : Step s₂ s₂✝
n : State.Nontrivial s₂
⊢ s₃✝ = s₂
Tactic:
cases ‹Step _ _›
State after:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝ : State α
e' : Steps s₂✝ s₂
e : s✝ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
exact absurd ht.symm $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
cases ‹Steps _ _›
State after:
case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
a✝ : s₂ ↓ᵢ| s₂✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₂✝.tag = s₂.tag → s₂✝.progress = s₂.progress → s₂✝ = s₂
ht : s₂✝.tag = s₂.tag
hp : s₂✝.progress = s₂.progress
⊢ s₂✝ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ e' : State α
n : State.Nontrivial e'
ht : e'.tag = s₂.tag
hp : e'.progress = s₂.progress
e : e' ↓ᵢ| s₂
⊢ e' = s₂
Tactic:
exact absurd hp $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝ : State α
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝
a_ih✝ : Steps s₂✝ s₂ → State.Nontrivial s₂✝ → s₂✝.tag = s₂.tag → s₂✝.progress = s₂.progress → s₂✝ = s₂
ht : s₂✝.tag = s₂.tag
hp : s₂✝.progress = s₂.progress
⊢ s₂✝ = s₂
Tactic:
exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₃✝ = s₂
Tactic:
cases ‹Step _ _›
State after:
case step.refl.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
a✝² : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s✝ = s₂
Tactic:
exact absurd ht $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₃✝ = s₂
Tactic:
exact absurd ht.symm $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s✝ : State α
n : State.Nontrivial s✝
ht : s✝.tag = s₂.tag
hp : s✝.progress = s₂.progress
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s✝ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ s₂✝¹ s₃✝ : State α
a_ih✝ : Steps s₂✝¹ s₂ → State.Nontrivial s₂✝¹ → s₃✝.tag = s₂.tag → s₃✝.progress = s₂.progress → s₃✝ = s₂
ht : s₃✝.tag = s₂.tag
hp : s₃✝.progress = s₂.progress
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₃✝ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
State after:
no goals