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

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

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
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
x y : M
h0 : f 1 = 0
⊢ 0 = 1
Tactic:
rw [← h, h0, Int.floor_zero]
State after:
no goals