Theorem: IMOSL.IMO2010A1.MonoidGood.solution_of_fract_map_one_pos (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
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]
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)

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
State after:
no goals

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 ↦ ?_⟩
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

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
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

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]
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

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
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

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
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

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
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

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
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

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 ↦ ?_
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

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⟩
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

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]
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

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
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

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]
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

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 _
State after:
no goals

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]
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}

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
State after:
no goals

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]
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

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
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}

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals