Theorem: Smt.Reconstruct.Arith.intTightLb' (Smt/Reconstruct/Arith/TightBounds/Lemmas.lean)

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {i : ℤ} {c : α}, ↑i > c → i ≥ ⌊c⌋ + 1
Tactic:
intros i c h
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
cases lt_trichotomy i (⌊c⌋ + 1) with
| inl iltc =>
  have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc
  simp at ilec
  have c_le_floor := Int.floor_le c
  have cast_ilec := le_trans (castLE' ilec) c_le_floor
  have abs := lt_of_le_of_lt cast_ilec h
  simp at abs
| inr h' => cases h' with
            | inl ieqc => exact le_of_eq (Eq.symm ieqc)
            | inr igtc => exact le_of_lt igtc
State after:
no goals

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc
State after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i + 1 ≤ ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i + 1 ≤ ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
simp at ilec
State after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
⊢ i ≥ ⌊c⌋ + 1

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have c_le_floor := Int.floor_le c
State after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
⊢ i ≥ ⌊c⌋ + 1

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have cast_ilec := le_trans (castLE' ilec) c_le_floor
State after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
⊢ i ≥ ⌊c⌋ + 1

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have abs := lt_of_le_of_lt cast_ilec h
State after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
abs : ↑i < ↑i
⊢ i ≥ ⌊c⌋ + 1

State before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
abs : ↑i < ↑i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
simp at abs
State after:
no goals

State before:
case inr
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
h' : i = ⌊c⌋ + 1 ∨ ⌊c⌋ + 1 < i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
cases h' with
| inl ieqc => exact le_of_eq (Eq.symm ieqc)
| inr igtc => exact le_of_lt igtc
State after:
no goals

State before:
case inr.inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
ieqc : i = ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
exact le_of_eq (Eq.symm ieqc)
State after:
no goals

State before:
case inr.inr
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
igtc : ⌊c⌋ + 1 < i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
exact le_of_lt igtc
State after:
no goals