internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : ∃ b ∈ h.rangeCompl, f^[m] b = a
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
⊢ a ≠ b
Tactic:
rcases h1 with ⟨a, h1, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
a : α
h1 : a ∈ h.rangeCompl
⊢ f^[m] a ≠ b
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
b : α
h2 : ∃ b_1 ∈ h.rangeCompl, f^[n] b_1 = b
a : α
h1 : a ∈ h.rangeCompl
⊢ f^[m] a ≠ b
Tactic:
rcases h2 with ⟨b, h2, rfl⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.rangeCompl
b : α
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b
Theorem: IMOSL.IMO2013A5.FinChainFn.exactIterRange_disjoint_of_ne
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
m n : ℕ
h0 : m ≠ n
a : α
h1 : a ∈ h.rangeCompl
b : α
h2 : b ∈ h.rangeCompl
⊢ f^[m] a ≠ f^[n] b
Tactic:
exact h.iter_apply_ne_of_mem_rangeCompl_iter_ne h0 h1 h2
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
⊢ ↑(h.iterRangeCompl 0) = (Set.range f^[0])ᶜ
Tactic:
rw [iterRangeCompl_zero, coe_empty,
  iterate_zero, Set.range_id, Set.compl_univ]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ ↑(h.iterRangeCompl (n + 1)) = (Set.range f^[n + 1])ᶜ
Tactic:
rw [h.iterRangeCompl_succ, coe_union, iterRangeCompl_spec n,
  h.exactIterRange_spec, Set.diff_eq, Set.inter_union_distrib_right,
  Set.union_compl_self, Set.univ_inter, ← Set.compl_inter]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (Set.range f^[n + 1] ∩ Set.range f^[n])ᶜ = (Set.range f^[n + 1])ᶜ
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (Set.range f^[n + 1] ∩ Set.range f^[n])ᶜ = (Set.range f^[n + 1])ᶜ
Tactic:
refine congr_arg _ (Set.inter_eq_left.mpr λ x h1 ↦ ?_)
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : x ∈ Set.range f^[n + 1]
⊢ x ∈ Set.range f^[n]
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : x ∈ Set.range f^[n + 1]
⊢ x ∈ Set.range f^[n]
Tactic:
rw [Set.mem_range] at h1 ⊢
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : ∃ y, f^[n + 1] y = x
⊢ ∃ y, f^[n] y = x
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
x : α
h1 : ∃ y, f^[n + 1] y = x
⊢ ∃ y, f^[n] y = x
Tactic:
rcases h1 with ⟨y, rfl⟩
Proof state after:
case intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
y : α
⊢ ∃ y_1, f^[n] y_1 = f^[n + 1] y
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_spec
Proof state before:
case intro
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
y : α
⊢ ∃ y_1, f^[n] y_1 = f^[n + 1] y
Tactic:
exact ⟨f y, rfl⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_card
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card
Tactic:
have h0 := card_union_of_disjoint
  (h.iterRangeCompl_disjoint_exactIterRange n.le_refl)
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
h0 : (h.exactIterRange n ∪ h.iterRangeCompl n).card = (h.exactIterRange n).card + (h.iterRangeCompl n).card
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card
Theorem: IMOSL.IMO2013A5.FinChainFn.iterRangeCompl_card
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
n : ℕ
h0 : (h.exactIterRange n ∪ h.iterRangeCompl n).card = (h.exactIterRange n).card + (h.iterRangeCompl n).card
⊢ (h.iterRangeCompl (n + 1)).card = (n + 1) * h.rangeCompl.card
Tactic:
rw [h.iterRangeCompl_succ, h0, h.exactIterRange_card,
  iterRangeCompl_card n, Nat.succ_mul, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_range_of_rangeCompl_singleton
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ h.iterRangeCompl (n + 1) = image (fun k => f^[k] a) (range (n + 1))
Tactic:
rw [h.iterRangeCompl_succ, exactIterRange, h0, image_singleton,
iter_range_of_rangeCompl_singleton h0 n, range_succ, image_insert]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ {f^[n] a} ∪ image (fun k => f^[k] a) (range n) = insert (f^[n] a) (image (fun k => f^[k] a) (range n))
Theorem: IMOSL.IMO2013A5.FinChainFn.iter_range_of_rangeCompl_singleton
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
h : FinChainFn f
a : α
h0 : h.rangeCompl = {a}
n : ℕ
⊢ {f^[n] a} ∪ image (fun k => f^[k] a) (range n) = insert (f^[n] a) (image (fun k => f^[k] a) (range n))
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.map_commute_of_commute
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Add S
inst✝¹ : Mul S
x y : R
inst✝ : IsCancelAdd S
f : R → S
h : good f
h0 : x * y = y * x
⊢ f x * f y + f (x + y) = f y * f x + f (x + y)
Tactic:
rw [← h, h0, h, add_comm x]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ReducedGood.period_imp_zero
Proof state before:
R : Type u_1
S : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : Add S
inst✝² : Mul S
inst✝¹ : One S
inst✝ : Zero S
c : R
f : R → S
hf : ReducedGood f
h : ∀ (x : R), f (x + c) = f x
x : R
⊢ f (x + c) = f (x + 0)
Tactic:
rw [h, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
have h1 n : N * (f (n + 1) - f n) = f N - f 0 := by
  rw [mul_sub, sub_eq_iff_eq_add, ← add_sub_right_comm, eq_sub_iff_add_eq',
    ← N.mul_zero, h0, zero_add, n.add_comm, ← h0, mul_one]
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
replace h1 n : f (n + 1) = (f 1 - f 0) + f n :=
  eq_add_of_sub_eq <| mul_left_cancel₀ h <| by rw [h1, ← h1 0, zero_add]
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), f (n + 1) = f 1 - f 0 + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), f (n + 1) = f 1 - f 0 + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
generalize f 1 - f 0 = q at h1
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f (n + 1) = q + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f (n + 1) = q + f n
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
apply Extra.IntIntLinearSolverAlt at h1
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
⊢ f = 0 ∨ ∃ c, f = fun x => N * x + c
Tactic:
refine (em' (N = q)).imp (λ h2 ↦ ?_) (λ h2 ↦ ⟨f 0, funext <| by rwa [h2]⟩)
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
⊢ f = 0
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
⊢ f = 0
Tactic:
have h3 := h0 0 0
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f (N * 0) + N * f 0 = f (f (0 + 0))
⊢ f = 0
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f (N * 0) + N * f 0 = f (f (0 + 0))
⊢ f = 0
Tactic:
rw [add_zero, N.mul_zero, h1 (f 0), add_comm, add_left_inj,
  mul_eq_mul_right_iff, or_iff_right h2] at h3
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
⊢ f = 0
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
⊢ f = 0
Tactic:
specialize h0 0 1
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : f (N * 0) + N * f 1 = f (f (0 + 1))
⊢ f = 0
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : f (N * 0) + N * f 1 = f (f (0 + 1))
⊢ f = 0
Tactic:
rw [N.mul_zero, zero_add, h1 (f 1), add_comm, add_left_inj,
  mul_eq_mul_right_iff, or_iff_right h2, h1, mul_one, h3, add_zero] at h0
Proof state after:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
⊢ f = 0
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
⊢ f = 0
Tactic:
funext n
Proof state after:
case h
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
n : ℤ
⊢ f n = 0 n
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
case h
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : ¬N = q
h3 : f 0 = 0
h0 : q = 0
n : ℤ
⊢ f n = 0 n
Tactic:
rw [h1, h0, h3, n.zero_mul, add_zero, Pi.zero_apply]
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
n : ℤ
⊢ N * (f (n + 1) - f n) = f N - f 0
Tactic:
rw [mul_sub, sub_eq_iff_eq_add, ← add_sub_right_comm, eq_sub_iff_add_eq',
  ← N.mul_zero, h0, zero_add, n.add_comm, ← h0, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
h1 : ∀ (n : ℤ), N * (f (n + 1) - f n) = f N - f 0
n : ℤ
⊢ N * (f (n + 1) - f n) = N * (f 1 - f 0)
Tactic:
rw [h1, ← h1 0, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : ∀ (a b : ℤ), f (N * a) + N * f b = f (f (a + b))
q : ℤ
h1 : ∀ (n : ℤ), f n = q * n + f 0
h2 : N = q
⊢ ∀ (x : ℤ), f x = N * x + f 0
Tactic:
rwa [h2]
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
N : ℤ
h : N ≠ 0
f : ℤ → ℤ
h0 : f = 0 ∨ ∃ c, f = fun x => N * x + c
a b : ℤ
⊢ f (N * a) + N * f b = f (f (a + b))
Tactic:
rcases h0 with rfl | ⟨c, rfl⟩
Proof state after:
case inl
N : ℤ
h : N ≠ 0
a b : ℤ
⊢ 0 (N * a) + N * 0 b = 0 (0 (a + b))

case inr.intro
N : ℤ
h : N ≠ 0
a b c : ℤ
⊢ (fun x => N * x + c) (N * a) + N * (fun x => N * x + c) b = (fun x => N * x + c) ((fun x => N * x + c) (a + b))
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
case inl
N : ℤ
h : N ≠ 0
a b : ℤ
⊢ 0 (N * a) + N * 0 b = 0 (0 (a + b))
Tactic:
exact (N * 0).zero_add.trans N.mul_zero
Proof state after:
no goals
Theorem: IMOSL.IMO2019A1.final_solution
Proof state before:
case inr.intro
N : ℤ
h : N ≠ 0
a b c : ℤ
⊢ (fun x => N * x + c) (N * a) + N * (fun x => N * x + c) b = (fun x => N * x + c) ((fun x => N * x + c) (a + b))
Tactic:
rw [add_right_comm, ← mul_add, ← add_assoc, ← mul_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤ₄.add_mul
Proof state before:
x y z : ℤ₄
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [ℤ₄.mul_comm, ℤ₄.mul_add, z.mul_comm, z.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤ₄.cast_add
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ 2 + 2 = 0
Tactic:
rw [← h, ← Nat.cast_two, ← Nat.cast_add]
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4
Theorem: IMOSL.IMO2012A5.ℤ₄.cast_add
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤ₄.cast_add
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h✝ : 4 = 0
x y : ℤ₄
h : 2 + 2 = 0
h0 : 1 + 1 = 2
⊢ -1 = 1 + 2
Tactic:
rwa [neg_eq_iff_add_eq_zero, ← add_assoc, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤ₄.cast_mul
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ 2 + 2 = 0
Tactic:
rw [← h, ← Nat.cast_two, ← Nat.cast_add]
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4
Theorem: IMOSL.IMO2012A5.ℤ₄.cast_mul
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
x y : ℤ₄
⊢ ↑(2 + 2) = 4
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤ₄.castRingHom_injective
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
h : 4 = 0
h0 : 2 ≠ 0
h1 : 1 = 0
⊢ 2 = 0
Tactic:
rw [← one_mul (2 : R), h1, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.castMonoidHom_is_MonoidGood
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : LinearOrderedRing R
inst✝¹ : FloorRing R
inst✝ : Mul M
φ : M →ₙ* ℤ
m n : M
⊢ (fun x => ↑(φ x)) (m * n) = (fun x => ↑(φ x)) m * ↑⌊(fun x => ↑(φ x)) n⌋
Tactic:
rw [Int.floor_intCast, ← Int.cast_mul, ← φ.map_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood
Proof 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 + ε) * _⌋
Proof 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)⌋
Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood
Proof 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]
Proof 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)⌋
Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood
Proof 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
Proof 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)⌋
Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A1.one_add_infinitesimal_mul_is_MonoidGood
Proof 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)⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (fun n => if n ∈ A then C else 0) (m * n) =
    (fun n => if n ∈ A then C else 0) m * ↑⌊(fun n => if n ∈ A then C else 0) n⌋
Tactic:
simp only [h]
Proof state after:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
by_cases h1 : n ∈ A
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋

case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
rw [if_pos h1, h0, Int.cast_one, mul_one]
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = if m ∈ A then C else 0
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∈ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = if m ∈ A then C else 0
Tactic:
exact if_congr (and_iff_left h1) rfl rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = (if m ∈ A then C else 0) * ↑⌊if n ∈ A then C else 0⌋
Tactic:
rw [if_neg h1, Int.floor_zero, Int.cast_zero, mul_zero]
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = 0
Theorem: IMOSL.IMO2010A1.indicator_const_is_good
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝³ : LinearOrderedRing R
inst✝² : FloorRing R
inst✝¹ : Mul M
C : R
A : Set M
inst✝ : DecidablePred fun x => x ∈ A
h : ∀ (m n : M), m * n ∈ A ↔ m ∈ A ∧ n ∈ A
h0 : ⌊C⌋ = 1
m n : M
h1 : n ∉ A
⊢ (if m ∈ A ∧ n ∈ A then C else 0) = 0
Tactic:
exact if_neg λ h2 ↦ h1 h2.2
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.map_eq_map_one_mul_floor
Proof 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
x : M
⊢ f x = f 1 * ↑⌊f x⌋
Tactic:
rw [← hf, one_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A1.MonoidGood.eq_zero_or_floor_map_one_eq_one
Proof 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]
Proof 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