Theorem: Smt.Reconstruct.Arith.intTightUb' (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:
have neg_c_lt_neg_i := Real.neg_lt_neg h
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have i_le_floor_neg_c: -i ≥ ⌊-c⌋ + 1 :=  by
  apply intTightLb'
  norm_cast at neg_c_lt_neg_i
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ ⌊-c⌋ + 1
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ ⌊-c⌋ + 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
rw [Int.floor_neg] at i_le_floor_neg_c
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have i_plus_one_le_c := Int.neg_le_neg i_le_floor_neg_c
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : - -i ≤ -(-⌈c⌉ + 1)
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : - -i ≤ -(-⌈c⌉ + 1)
⊢ i ≤ ⌈c⌉ - 1
Tactic:
simp at i_plus_one_le_c
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : 1 + i ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : 1 + i ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Tactic:
rw [add_comm] at i_plus_one_le_c
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have pf: i + 1 - 1 ≤ ⌈c⌉ - 1 := Int.add_le_add i_plus_one_le_c le_rfl
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i + 1 - 1 ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i + 1 - 1 ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
simp at pf
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
exact pf
State after:
no goals

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ -i ≥ ⌊-c⌋ + 1
Tactic:
apply intTightLb'
State after:
case a
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ ↑(-i) > -c

State before:
case a
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ ↑(-i) > -c
Tactic:
norm_cast at neg_c_lt_neg_i
State after:
no goals