Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered (IMOSLLean4/IMO2010/A1/A1Dense.lean)

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

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

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 ↦ ?_)
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

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

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

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
State after:
no goals

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 ↦ ?_⟩
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

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]
State after:
no goals

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

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

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

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

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

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

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
State after:
no goals

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

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

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

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
State after:
no goals

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

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

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
State after:
no goals

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]
State after:
no goals

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

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)⌋
⊢ -1 ≤ -c ∧ -c < 0
Tactic:
exact ⟨neg_le_neg hc.2.le, neg_lt_zero.mpr hc.1⟩
State after:
no goals

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✝ : (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
x✝² : ∃ C, ⌊C⌋ = 1 ∧ f = fun x => C
x✝¹ x✝ : R
C : S
h : ⌊C⌋ = 1
h0 : f = fun x => C
⊢ f (⌊x✝¹⌋ • x✝) = f x✝¹ * ↑⌊f x✝⌋
Tactic:
rw [h0, h, Int.cast_one, mul_one]
State after:
no goals