Theorem: IMOSL.IMO2010A1.MonoidGood.floor_unbounded_of_one_lt (IMOSLLean4/IMO2010/A1/A1Monoid.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
⊢ ∃ y, ↑(N + 1) < ⌊f y⌋
Tactic:
rcases floor_unbounded_of_one_lt h0 N with ⟨y, h1⟩
State after:
case intro
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ ∃ y, ↑(N + 1) < ⌊f y⌋

State before:
case intro
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ ∃ y, ↑(N + 1) < ⌊f y⌋
Tactic:
use x * y
State after:
case h
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ ↑(N + 1) < ⌊f (x * y)⌋

State before:
case h
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ ↑(N + 1) < ⌊f (x * y)⌋
Tactic:
rw [floor_map_mul hf h, Nat.cast_succ, ← one_mul ((N : ℤ) + 1)]
State after:
case h
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ 1 * (↑N + 1) < ⌊f x⌋ * ⌊f y⌋

State before:
case h
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf : MonoidGood f
h : ⌊f 1⌋ = 1
x : M
h0 : 1 < ⌊f x⌋
N : ℕ
y : M
h1 : ↑N < ⌊f y⌋
⊢ 1 * (↑N + 1) < ⌊f x⌋ * ⌊f y⌋
Tactic:
exact mul_lt_mul_of_nonneg_of_pos h0 h1 Int.one_nonneg (N.cast_nonneg.trans_lt h1)
State after:
no goals