Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood (IMOSLLean4/IMO2010/A1/A1Monoid.lean)

State before:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ (fun x => (1 + ε) * ↑(φ x)) (m * n) = (fun x => (1 + ε) * ↑(φ x)) m * ↑⌊(fun x => (1 + ε) * ↑(φ x)) n⌋
Tactic:
change (1 + ε) * _ = (1 + ε) * _ * ⌊(1 + ε) * _⌋
State after:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ (1 + ε) * ↑(φ (m * n)) = (1 + ε) * ↑(φ m) * ↑⌊(1 + ε) * ↑(φ n)⌋

State before:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ (1 + ε) * ↑(φ (m * n)) = (1 + ε) * ↑(φ m) * ↑⌊(1 + ε) * ↑(φ n)⌋
Tactic:
rw [φ.map_mul, Nat.cast_mul, ← mul_assoc]
State after:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ (1 + ε) * ↑(φ m) * ↑(φ n) = (1 + ε) * ↑(φ m) * ↑⌊(1 + ε) * ↑(φ n)⌋

State before:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ (1 + ε) * ↑(φ m) * ↑(φ n) = (1 + ε) * ↑(φ m) * ↑⌊(1 + ε) * ↑(φ n)⌋
Tactic:
apply congrArg
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ ↑(φ n) = ↑⌊(1 + ε) * ↑(φ n)⌋

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ ↑(φ n) = ↑⌊(1 + ε) * ↑(φ n)⌋
Tactic:
rw [one_add_mul ε, Int.floor_nat_add, Int.cast_add, Int.cast_natCast,
  ← nsmul_eq_mul', self_eq_add_right, Int.cast_eq_zero, Int.floor_eq_zero_iff]
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ φ n • ε ∈ Set.Ico 0 1

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℕ
ε : R
h : 0 ≤ ε
h0 : Infinitesimal ε
m n : M
⊢ φ n • ε ∈ Set.Ico 0 1
Tactic:
exact ⟨nsmul_nonneg h _, abs_eq_self.mpr h ▸ h0 (φ n)⟩
State after:
no goals