Theorem: round_eq_trunc_of_le (Fl/Round.lean)

State before:
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
⊢ round x = trunc n x
Tactic:
cases hfaithful₁ x with
| inl hlo => exact hlo
| inr hhi =>
  exfalso
  apply Nat.lt_le_asymm (lt_next_trunc npos x)
  exact hhi ▸ h
State after:
no goals

State before:
case inl
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hlo : round x = trunc n x
⊢ round x = trunc n x
Tactic:
exact hlo
State after:
no goals

State before:
case inr
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ round x = trunc n x
Tactic:
exfalso
State after:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ False

State before:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ False
Tactic:
apply Nat.lt_le_asymm (lt_next_trunc npos x)
State after:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ next n (trunc n x) ≤ x

State before:
case inr.h
n x : ℕ
npos : 0 < n
round : ℕ → ℕ
hfaithful₁ : faithful₁ n round
h : round x ≤ x
hhi : round x = next n (trunc n x)
⊢ next n (trunc n x) ≤ x
Tactic:
exact hhi ▸ h
State after:
no goals