Theorem: round_le_trunc_of_le_trunc (Fl/Round.lean)

State before:
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
⊢ round y ≤ trunc n x
Tactic:
cases Nat.lt_or_eq_of_le h with
| inl lt => have pos := Nat.zero_lt_of_lt lt
  rewrite [← next_trunc_pred_trunc_eq_self npos pos]
  apply Nat.le_trans
  . exact round_le_next_trunc hfaithful₁ y
  . apply next_le_next
    apply trunc_le_trunc npos
    apply Nat.le_pred_of_lt
    exact lt
| inr eq => rw [eq, round_trunc npos x hfaithful₀]
State after:
no goals

State before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
⊢ round y ≤ trunc n x
Tactic:
have pos := Nat.zero_lt_of_lt lt
State after:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ trunc n x

State before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ trunc n x
Tactic:
rewrite [← next_trunc_pred_trunc_eq_self npos pos]
State after:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ next n (trunc n (trunc n x - 1))

State before:
case inl
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ next n (trunc n (trunc n x - 1))
Tactic:
apply Nat.le_trans
State after:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m

case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ?inl.m ≤ next n (trunc n (trunc n x - 1))

case inl.m
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ℕ

State before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m

case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ?inl.m ≤ next n (trunc n (trunc n x - 1))

case inl.m
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ ℕ
Tactic:
. exact round_le_next_trunc hfaithful₁ y
State after:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))

State before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
Tactic:
. apply next_le_next
  apply trunc_le_trunc npos
  apply Nat.le_pred_of_lt
  exact lt
State after:
no goals

State before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ round y ≤ ?inl.m
Tactic:
exact round_le_next_trunc hfaithful₁ y
State after:
no goals

State before:
case inl.a
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ next n (trunc n y) ≤ next n (trunc n (trunc n x - 1))
Tactic:
apply next_le_next
State after:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ trunc n y ≤ trunc n (trunc n x - 1)

State before:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ trunc n y ≤ trunc n (trunc n x - 1)
Tactic:
apply trunc_le_trunc npos
State after:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y ≤ trunc n x - 1

State before:
case inl.a.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y ≤ trunc n x - 1
Tactic:
apply Nat.le_pred_of_lt
State after:
case inl.a.h.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y < Nat.sub (trunc n x) 0

State before:
case inl.a.h.h
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
lt : y < trunc n x
pos : 0 < trunc n x
⊢ y < Nat.sub (trunc n x) 0
Tactic:
exact lt
State after:
no goals

State before:
case inr
n x y : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
h : y ≤ trunc n x
eq : y = trunc n x
⊢ round y ≤ trunc n x
Tactic:
rw [eq, round_trunc npos x hfaithful₀]
State after:
no goals