Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one (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
⊢ f = 0 ∨ ⌊f 1⌋ = 1
Tactic:
have h := map_eq_map_one_mul_floor hf 1
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 = f 1 * ↑⌊f 1⌋
⊢ f = 0 ∨ ⌊f 1⌋ = 1

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 = f 1 * ↑⌊f 1⌋
⊢ f = 0 ∨ ⌊f 1⌋ = 1
Tactic:
rw [← sub_eq_zero, ← mul_one_sub, mul_eq_zero] at h
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 = 0 ∨ 1 - ↑⌊f 1⌋ = 0
⊢ f = 0 ∨ ⌊f 1⌋ = 1

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 ∨ 1 - ↑⌊f 1⌋ = 0
⊢ f = 0 ∨ ⌊f 1⌋ = 1
Tactic:
revert h
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
⊢ f 1 = 0 ∨ 1 - ↑⌊f 1⌋ = 0 → f = 0 ∨ ⌊f 1⌋ = 1

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
⊢ f 1 = 0 ∨ 1 - ↑⌊f 1⌋ = 0 → f = 0 ∨ ⌊f 1⌋ = 1
Tactic:
refine Or.imp (λ h ↦ funext λ n ↦ ?_)
(λ h ↦ Int.cast_eq_one.mp (eq_of_sub_eq_zero h).symm)
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 = 0
n : M
⊢ f n = 0 n

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
⊢ f n = 0 n
Tactic:
rw [map_eq_map_one_mul_floor hf, h, zero_mul]
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 = 0
n : M
⊢ 0 = 0 n

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