internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2010A1.MonoidGood.solution
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A3.iterate_add_mul_eq
Proof state before:
n k : ℕ
S : Type u_1
f : S → S
h : f^[n + k] = f^[n]
t : ℕ
⊢ f^[n + k * (t + 1)] = f^[n]
Tactic:
rw [k.mul_succ, ← Nat.add_assoc, f.iterate_add,
iterate_add_mul_eq h t, ← f.iterate_add, h]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A3.range_iter_two_eq_of_exists_iter_eq_self
Proof state before:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f^[2] = Set.range f
Tactic:
apply (Set.range_comp_subset_range f f).antisymm
Proof state after:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Theorem: IMOSL.IMO2017A3.range_iter_two_eq_of_exists_iter_eq_self
Proof state before:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
Proof state after:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Theorem: IMOSL.IMO2017A3.range_iter_two_eq_of_exists_iter_eq_self
Proof state before:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Tactic:
nth_rw 1 [← h0, f.iterate_add]
Proof state after:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range (f^[2] ∘ f^[k]) ⊆ Set.range (f ∘ f)
Theorem: IMOSL.IMO2017A3.range_iter_two_eq_of_exists_iter_eq_self
Proof state before:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range (f^[2] ∘ f^[k]) ⊆ Set.range (f ∘ f)
Tactic:
exact Set.range_comp_subset_range _ _
Proof state after:
no goals
Theorem: IMOSL.IMO2017A3.exists_lt_iterate_eq
Proof state before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]
Tactic:
obtain ⟨a, b, h, h0⟩ : ∃ a b : ℕ, a ≠ b ∧ f^[a] = f^[b] :=
  Finite.exists_ne_map_eq_of_infinite _
Proof state after:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a ≠ b
h0 : f^[a] = f^[b]
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]
Theorem: IMOSL.IMO2017A3.exists_lt_iterate_eq
Proof state before:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a ≠ b
h0 : f^[a] = f^[b]
⊢ ∃ a b, a < b ∧ f^[a] = f^[b]
Tactic:
exact h.lt_or_lt.elim (λ h ↦ ⟨a, b, h, h0⟩) (λ h ↦ ⟨b, a, h, h0.symm⟩)
Proof state after:
no goals
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
obtain ⟨a, b, h, h0⟩ := exists_lt_iterate_eq f
Proof state after:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a < b
h0 : f^[a] = f^[b]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a < b
h0 : f^[a] = f^[b]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
rcases Nat.exists_eq_add_of_le h.le with ⟨c, rfl⟩
Proof state after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : a < a + c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : a < a + c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
rw [Nat.lt_add_right_iff_pos] at h
Proof state after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
refine ⟨c * a.succ, Nat.mul_pos h a.succ_pos, ?_⟩
Proof state after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[2 * (c * a.succ)] = f^[c * a.succ]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[2 * (c * a.succ)] = f^[c * a.succ]
Tactic:
rw [Nat.two_mul]
Proof state after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c * a.succ] = f^[c * a.succ]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c * a.succ] = f^[c * a.succ]
Tactic:
refine iterate_add_mul_eq ?_ _
Proof state after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Tactic:
obtain ⟨k, h1⟩ := Nat.exists_eq_add_of_le
  (Nat.le_mul_of_pos_left a.succ h)
Proof state after:
case intro.intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
k : ℕ
h1 : c * a.succ = a.succ + k
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent
Proof state before:
case intro.intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
k : ℕ
h1 : c * a.succ = a.succ + k
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Tactic:
rw [h1, Nat.add_right_comm, f.iterate_add, Nat.succ_add,
  f.iterate_succ, ← h0, ← f.iterate_succ, f.iterate_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A3.final_solution
Proof state before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
⊢ Set.range f^[2] = Set.range f
Tactic:
rcases exists_iterate_idempotent f with ⟨n, h0, h1⟩
Proof state after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ Set.range f^[2] = Set.range f
Theorem: IMOSL.IMO2017A3.final_solution
Proof state before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ Set.range f^[2] = Set.range f
Tactic:
refine range_iter_two_eq_of_exists_iter_eq_self
  (Nat.lt_add_of_pos_left h0) (h _ ?_)
Proof state after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1] ∘ f ∘ f^[n + 1]
Theorem: IMOSL.IMO2017A3.final_solution
Proof state before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1] ∘ f ∘ f^[n + 1]
Tactic:
rw [← f.iterate_succ', ← f.iterate_add]
Proof state after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1 + (n + 1).succ]
Theorem: IMOSL.IMO2017A3.final_solution
Proof state before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1 + (n + 1).succ]
Tactic:
change (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]
Proof state after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]
Theorem: IMOSL.IMO2017A3.final_solution
Proof state before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]
Tactic:
rw [Nat.succ_add, ← Nat.two_mul, f.iterate_succ' (2 * n), h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
⊢ (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
Tactic:
have h0 : ⌊f 0⌋ = 1 ∨ f 0 = 0 := by
  have h0 := h 0 0
  rw [zsmul_zero, ← sub_eq_zero, ← mul_one_sub, mul_eq_zero] at h0
  exact h0.symm.imp_left λ h0 ↦ Int.cast_eq_one.mp (eq_of_sub_eq_zero h0).symm
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1 ∨ f 0 = 0
⊢ (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1 ∨ f 0 = 0
⊢ (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
Tactic:
revert h0
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0 → (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0 → (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
Tactic:
refine Or.imp (λ h0 ↦ ?_) (λ h0 ↦ ?_)
Proof state after:
case refine_1
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1
⊢ ∃ C, ⌊C⌋ = 1 ∧ f = fun x => C

case refine_2
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0
⊢ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0
Tactic:
have h0 := h 0 0
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f (⌊0⌋ • 0) = f 0 * ↑⌊f 0⌋
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f (⌊0⌋ • 0) = f 0 * ↑⌊f 0⌋
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0
Tactic:
rw [zsmul_zero, ← sub_eq_zero, ← mul_one_sub, mul_eq_zero] at h0
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0 ∨ 1 - ↑⌊f 0⌋ = 0
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0 ∨ 1 - ↑⌊f 0⌋ = 0
⊢ ⌊f 0⌋ = 1 ∨ f 0 = 0
Tactic:
exact h0.symm.imp_left λ h0 ↦ Int.cast_eq_one.mp (eq_of_sub_eq_zero h0).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_1
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1
⊢ ∃ C, ⌊C⌋ = 1 ∧ f = fun x => C
Tactic:
refine ⟨f 0, h0, funext λ x ↦ ?_⟩
Proof state after:
case refine_1
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1
x : R
⊢ f x = f 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_1
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : ⌊f 0⌋ = 1
x : R
⊢ f x = f 0
Tactic:
rw [← zsmul_zero ⌊x⌋, h, h0, Int.cast_one, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0
⊢ f = 0
Tactic:
rcases exists_between (zero_lt_one' R) with ⟨c, hc⟩
Proof state after:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
⊢ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
⊢ f = 0
Tactic:
replace h0 : ⌊f c⌋ = 0 := by
  specialize h c c
  have h1 : ⌊c⌋ = 0 := Int.floor_eq_zero_iff.mpr ⟨hc.1.le, hc.2⟩
  rw [h1, zero_zsmul, h0, zero_eq_mul] at h
  exact h.elim (λ h ↦ h ▸ Int.floor_zero) Int.cast_eq_zero.mp
Proof state after:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
⊢ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
⊢ f = 0
Tactic:
replace h0 : f (-c) = 0 := by
  specialize h (-1) c
  have h1 : ⌊(-1 : R)⌋ = -1 := by
    rw [← Int.cast_one, ← Int.cast_neg, Int.floor_intCast]
  rwa [h1, neg_one_zsmul, h0, Int.cast_zero, mul_zero] at h
Proof state after:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
⊢ f = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
⊢ f = 0
Tactic:
funext y
Proof state after:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
⊢ f y = 0 y
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
⊢ f y = 0 y
Tactic:
specialize h (-c) (-y)
Proof state after:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
⊢ f y = 0 y
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
⊢ f y = 0 y
Tactic:
have h1 : ⌊-c⌋ = -1 := by
  rw [Int.floor_eq_iff, Int.cast_neg, Int.cast_one, neg_add_self]
  exact ⟨neg_le_neg hc.2.le, neg_lt_zero.mpr hc.1⟩
Proof state after:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
h1 : ⌊-c⌋ = -1
⊢ f y = 0 y
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
case refine_2.intro.h
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
h1 : ⌊-c⌋ = -1
⊢ f y = 0 y
Tactic:
rwa [h0, zero_mul, h1, neg_one_zsmul, neg_neg] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
⊢ ⌊f c⌋ = 0
Tactic:
specialize h c c
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f (⌊c⌋ • c) = f c * ↑⌊f c⌋
⊢ ⌊f c⌋ = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f (⌊c⌋ • c) = f c * ↑⌊f c⌋
⊢ ⌊f c⌋ = 0
Tactic:
have h1 : ⌊c⌋ = 0 := Int.floor_eq_zero_iff.mpr ⟨hc.1.le, hc.2⟩
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f (⌊c⌋ • c) = f c * ↑⌊f c⌋
h1 : ⌊c⌋ = 0
⊢ ⌊f c⌋ = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f (⌊c⌋ • c) = f c * ↑⌊f c⌋
h1 : ⌊c⌋ = 0
⊢ ⌊f c⌋ = 0
Tactic:
rw [h1, zero_zsmul, h0, zero_eq_mul] at h
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f c = 0 ∨ ↑⌊f c⌋ = 0
h1 : ⌊c⌋ = 0
⊢ ⌊f c⌋ = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h0 : f 0 = 0
c : R
hc : 0 < c ∧ c < 1
h : f c = 0 ∨ ↑⌊f c⌋ = 0
h1 : ⌊c⌋ = 0
⊢ ⌊f c⌋ = 0
Tactic:
exact h.elim (λ h ↦ h ▸ Int.floor_zero) Int.cast_eq_zero.mp
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h : good f
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
⊢ f (-c) = 0
Tactic:
specialize h (-1) c
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
h : f (⌊-1⌋ • c) = f (-1) * ↑⌊f c⌋
⊢ f (-c) = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
h : f (⌊-1⌋ • c) = f (-1) * ↑⌊f c⌋
⊢ f (-c) = 0
Tactic:
have h1 : ⌊(-1 : R)⌋ = -1 := by
  rw [← Int.cast_one, ← Int.cast_neg, Int.floor_intCast]
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
h : f (⌊-1⌋ • c) = f (-1) * ↑⌊f c⌋
h1 : ⌊-1⌋ = -1
⊢ f (-c) = 0
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
h : f (⌊-1⌋ • c) = f (-1) * ↑⌊f c⌋
h1 : ⌊-1⌋ = -1
⊢ f (-c) = 0
Tactic:
rwa [h1, neg_one_zsmul, h0, Int.cast_zero, mul_zero] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : ⌊f c⌋ = 0
h : f (⌊-1⌋ • c) = f (-1) * ↑⌊f c⌋
⊢ ⌊-1⌋ = -1
Tactic:
rw [← Int.cast_one, ← Int.cast_neg, Int.floor_intCast]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
⊢ ⌊-c⌋ = -1
Tactic:
rw [Int.floor_eq_iff, Int.cast_neg, Int.cast_one, neg_add_self]
Proof state after:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
⊢ -1 ≤ -c ∧ -c < 0