internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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 = 0
n : M
⊢ 0 = 0 n
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.fract_eq_eps_mul_floor
Proof 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
⊢ Int.fract (f x) = Int.fract (f 1) * ↑⌊f x⌋
Tactic:
rw [Int.fract, Int.fract, h, Int.cast_one, sub_one_mul, ← map_eq_map_one_mul_floor hf]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_map_mul
Proof 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 y : M
⊢ ⌊f (x * y)⌋ = ⌊f x⌋ * ⌊f y⌋
Tactic:
have h0 : f 1 ≠ 0 := λ h0 ↦ Int.zero_ne_one <| by rw [← h, h0, Int.floor_zero]
Proof state after:
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 y : M
h0 : f 1 ≠ 0
⊢ ⌊f (x * y)⌋ = ⌊f x⌋ * ⌊f y⌋
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_map_mul
Proof 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 y : M
h0 : f 1 ≠ 0
⊢ ⌊f (x * y)⌋ = ⌊f x⌋ * ⌊f y⌋
Tactic:
have h1 := hf x y
Proof state after:
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 y : M
h0 : f 1 ≠ 0
h1 : f (x * y) = f x * ↑⌊f y⌋
⊢ ⌊f (x * y)⌋ = ⌊f x⌋ * ⌊f y⌋
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_map_mul
Proof 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 y : M
h0 : f 1 ≠ 0
h1 : f (x * y) = f x * ↑⌊f y⌋
⊢ ⌊f (x * y)⌋ = ⌊f x⌋ * ⌊f y⌋
Tactic:
rwa [map_eq_map_one_mul_floor hf, map_eq_map_one_mul_floor hf x, mul_assoc, ← sub_eq_zero,
  ← mul_sub, mul_eq_zero, or_iff_right h0, ← Int.cast_mul, sub_eq_zero, Int.cast_inj] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_map_mul
Proof 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 y : M
h0 : f 1 = 0
⊢ 0 = 1
Tactic:
rw [← h, h0, Int.floor_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_unbounded_of_one_lt
Proof 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⟩
Proof 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⌋
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_unbounded_of_one_lt
Proof 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
Proof 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)⌋
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_unbounded_of_one_lt
Proof 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)]
Proof 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⌋
Theorem: IMOSL.IMO2010A1.MonoidGood.floor_unbounded_of_one_lt
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof 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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
⊢ f x = f 1 * ↑({ toFun := fun x => ⌊f x⌋.natAbs, map_one' := ⋯, map_mul' := ⋯ } x)
Tactic:
rw [map_eq_map_one_mul_floor hf,
← Int.natAbs_of_nonneg (h1 x), Int.cast_natCast]
Proof state after:
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
⊢ f 1 * ↑⌊f x⌋.natAbs = f 1 * ↑({ toFun := fun x => ⌊f x⌋.natAbs, map_one' := ⋯, map_mul' := ⋯ } x)
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof 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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
⊢ f 1 * ↑⌊f x⌋.natAbs = f 1 * ↑({ toFun := fun x => ⌊f x⌋.natAbs, map_one' := ⋯, map_mul' := ⋯ } x)
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof 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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
⊢ ∃ A, ∃ (_ : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A), ∀ (x : M), f x = if x ∈ A then f 1 else 0
Tactic:
refine ⟨{x : M | ⌊f x⌋ ≠ 0}, λ x y ↦ ?_, λ x ↦ ?_⟩
Proof state after:
case refine_1
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x y : M
⊢ x * y ∈ {x | ⌊f x⌋ ≠ 0} ↔ x ∈ {x | ⌊f x⌋ ≠ 0} ∧ y ∈ {x | ⌊f x⌋ ≠ 0}

case refine_2
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case refine_2
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Tactic:
by_cases h3 : ⌊f x⌋ = 0
Proof state after:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0

case neg
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Tactic:
suffices ⌊f x⌋ = 1 by rw [if_pos (by rwa [Set.mem_setOf_eq]),
  map_eq_map_one_mul_floor hf, this, Int.cast_one, mul_one]
Proof state after:
case neg
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
⊢ ⌊f x⌋ = 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
⊢ ⌊f x⌋ = 1
Tactic:
specialize h1 x
Proof state after:
case neg
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 0 ≤ ⌊f x⌋
⊢ ⌊f x⌋ = 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 0 ≤ ⌊f x⌋
⊢ ⌊f x⌋ = 1
Tactic:
rw [le_iff_eq_or_lt, eq_comm, or_iff_right h3,
Int.lt_iff_add_one_le, zero_add, le_iff_eq_or_lt] at h1
Proof state after:
case neg
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 = ⌊f x⌋ ∨ 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 = ⌊f x⌋ ∨ 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Tactic:
rcases h1 with h1 | h1
Proof state after:
case neg.inl
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 = ⌊f x⌋
⊢ ⌊f x⌋ = 1

case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inl
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 = ⌊f x⌋
⊢ ⌊f x⌋ = 1

case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Tactic:
exact h1.symm
Proof state after:
case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
⊢ ⌊f x⌋ = 1
Tactic:
refine h2.elim λ N ↦ ?_
Proof state after:
case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
⊢ N • Int.fract (f 1) < 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr
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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
⊢ N • Int.fract (f 1) < 1
Tactic:
rcases floor_unbounded_of_one_lt hf h h1 N with ⟨y, h4⟩
Proof state after:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ N • Int.fract (f 1) < 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ N • Int.fract (f 1) < 1
Tactic:
rw [nsmul_eq_mul', ← Int.cast_natCast]
Proof state after:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f 1) * ↑↑N < 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f 1) * ↑↑N < 1
Tactic:
apply (mul_lt_mul_of_pos_left (Int.cast_lt.mpr h4) h0).trans
Proof state after:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f 1) * ↑⌊f y⌋ < 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f 1) * ↑⌊f y⌋ < 1
Tactic:
rw [← fract_eq_eps_mul_floor hf h]
Proof state after:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f y) < 1
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case neg.inr.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
h0 : 0 < Int.fract (f 1)
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
h1 : 1 < ⌊f x⌋
N : ℕ
y : M
h4 : ↑N < ⌊f y⌋
⊢ Int.fract (f y) < 1
Tactic:
exact Int.fract_lt_one _
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case refine_1
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x y : M
⊢ x * y ∈ {x | ⌊f x⌋ ≠ 0} ↔ x ∈ {x | ⌊f x⌋ ≠ 0} ∧ y ∈ {x | ⌊f x⌋ ≠ 0}
Tactic:
rw [Set.mem_setOf_eq, floor_map_mul hf h, mul_ne_zero_iff]
Proof state after:
case refine_1
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x y : M
⊢ ⌊f x⌋ ≠ 0 ∧ ⌊f y⌋ ≠ 0 ↔ x ∈ {x | ⌊f x⌋ ≠ 0} ∧ y ∈ {x | ⌊f x⌋ ≠ 0}
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case refine_1
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x y : M
⊢ ⌊f x⌋ ≠ 0 ∧ ⌊f y⌋ ≠ 0 ↔ x ∈ {x | ⌊f x⌋ ≠ 0} ∧ y ∈ {x | ⌊f x⌋ ≠ 0}
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Tactic:
rw [map_eq_map_one_mul_floor hf, h3, Int.cast_zero, mul_zero]
Proof state after:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ 0 = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ 0 = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Tactic:
refine (if_neg ?_).symm
Proof state after:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ x ∉ {x | ⌊f x⌋ ≠ 0}
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof state before:
case pos
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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ⌊f x⌋ = 0
⊢ x ∉ {x | ⌊f x⌋ ≠ 0}
Tactic:
rwa [Set.mem_setOf_eq, not_not]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof 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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
this : ⌊f x⌋ = 1
⊢ f x = if x ∈ {x | ⌊f x⌋ ≠ 0} then f 1 else 0
Tactic:
rw [if_pos (by rwa [Set.mem_setOf_eq]),
map_eq_map_one_mul_floor hf, this, Int.cast_one, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos
Proof 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
h0 : 0 < Int.fract (f 1)
h1 : ∀ (x : M), 0 ≤ ⌊f x⌋
h2 : ¬∀ (k : ℕ), k • Int.fract (f 1) < 1
x : M
h3 : ¬⌊f x⌋ = 0
this : ⌊f x⌋ = 1
⊢ x ∈ {x | ⌊f x⌋ ≠ 0}
Tactic:
rwa [Set.mem_setOf_eq]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof 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 = 0
x✝¹ x✝ : M
⊢ x✝¹ * x✝ ∈ ∅ ↔ x✝¹ ∈ ∅ ∧ x✝ ∈ ∅
Tactic:
simp only [Set.mem_empty_iff_false, and_self]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof 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 = 0
x : M
⊢ f x = if x ∈ ∅ then 1 else 0
Tactic:
rw [Set.mem_empty_iff_false, if_false, h]
Proof state after:
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 = 0
x : M
⊢ 0 x = 0
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof 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 = 0
x : M
⊢ 0 x = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof 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
h0 : 0 < Int.fract (f 1)
x✝ : Infinitesimal (Int.fract (f 1)) ∧ ∃ φ, ∀ (x : M), f x = f 1 * ↑(φ x)
h1 : Infinitesimal (Int.fract (f 1))
h2 : ∃ φ, ∀ (x : M), f x = f 1 * ↑(φ x)
φ : M →* ℕ
h3 : ∀ (x : M), f x = f 1 * ↑(φ x)
y : M
⊢ f y = (1 + Int.fract (f 1)) * ↑(φ y)
Tactic:
rw [h3, ← Int.cast_one, ← h, Int.floor_add_fract]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
f : M → R
hf :
  (∃ φ, f = fun x => ↑(φ x)) ∨
    (∃ ε, ∃ (_ : 0 < ε) (_ : Infinitesimal ε), ∃ φ, f = fun x => (1 + ε) * ↑(φ x)) ∨
      ∃ A, ∃ (_ : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A), ∃ C, ∃ (_ : ⌊C⌋ = 1), f = fun x => if x ∈ A then C else 0
⊢ MonoidGood f
Tactic:
rcases hf with ⟨φ, rfl⟩ | ⟨ε, hε, hε0, φ, rfl⟩ | ⟨A, hA, C, hC, rfl⟩
Proof state after:
case inl.intro
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
φ : M →* ℤ
⊢ MonoidGood fun x => ↑(φ x)

case inr.inl.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
ε : R
hε : 0 < ε
hε0 : Infinitesimal ε
φ : M →* ℕ
⊢ MonoidGood fun x => (1 + ε) * ↑(φ x)

case inr.inr.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : MulOneClass M
A : Set M
hA : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
C : R
hC : ⌊C⌋ = 1
⊢ MonoidGood fun x => if x ∈ A then C else 0