Theorem: IMOSL.IMO2010A1.MonoidGood.solution (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 = 0
x✝¹ x✝ : M
⊢ x✝¹ * x✝ ∈ ∅ ↔ x✝¹ ∈ ∅ ∧ x✝ ∈ ∅
Tactic:
simp only [Set.mem_empty_iff_false, and_self]
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 = 0
x : M
⊢ f x = if x ∈ ∅ then 1 else 0
Tactic:
rw [Set.mem_empty_iff_false, if_false, 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 = 0
x : M
⊢ 0 x = 0

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
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)
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]
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 :
  (∃ φ, 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⟩
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

State before:
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
Tactic:
exacts [castMonoidHom_is_MonoidGood φ.toMulHom,
  one_add_infinitesimal_mul_is_MonoidGood φ.toMulHom hε.le hε0,
  indicator_const_is_good hA hC]
State after:
no goals