IMO 2024 P6

Let \mathbb{Q} be the set of rational numbers. A function f : \mathbb{Q} \to \mathbb{Q} is called aquaesulian if the following property holds: for every x, y \in \mathbb{Q}, f(x + f(y)) = f(x) + y \qquad\text{or}\qquad f(f(x) + y) = x + f(y). Show that there exists an integer c such that for any aquaesulian function f there are at most c different rational numbers of the form f(r) + f(-r) for some rational number r, and find the smallest possible value of c.

Solution: c=2

open Polynomial

theorem imo_2024_p6
    (IsAquaesulian : (ℚ → ℚ) → Prop)
    (IsAquaesulian_def : ∀ f, IsAquaesulian f ↔
      ∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) :
    IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧
      {(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2 := byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ IsLeast
  {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2
  exists@?_refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ 2 ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}
refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ 2 ∈
  lowerBounds
    {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}
  ·refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ 2 ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} /- Let f be an aquaesulian function with f(0) = 0.
       We claim that f(x) + f(-x) takes on at most two distinct values. -/
    useλu b=>if j:u 0=0then by_contra λc=>?_ else ?_refine_1.refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
⊢ False
refine_1.refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : ¬u 0 = 0
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
    ·refine_1.refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
⊢ False -- If f(x) + f(-x) = 0 for all x, we are done.
      suffices:({J|∃k,u k+u (-k)= J}) ⊆{0}refine_1.refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
this : {J | ∃ k, u k + u (-k) = J} ⊆ {0}
⊢ False
this
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
⊢ {J | ∃ k, u k + u (-k) = J} ⊆ {0}
      ·refine_1.refine_1
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
this : {J | ∃ k, u k + u (-k) = J} ⊆ {0}
⊢ False simp_all[this.antisymm]All goals completed! 🐙
      -- Otherwise, take a, k such that f(a) + f(-a) = k ≠ 0.
      rintro - ⟨a, rfl⟩this.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
c : ¬({x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2)
a : ℚ
⊢ u a + u (-a) ∈ {0}
      contrapose! cthis.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : IsAquaesulian u
j : u 0 = 0
a : ℚ
c : u a + u (-a) ∉ {0}
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ ↑{x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
      simp_allthis.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
      -- If we can show that f(x) + f(-x) = 0 or k for all x, then we are done.
      suffices:{U|∃examples6, (u) ‹ℚ› +u ( -‹_›)= U} ⊆{0,(u (a : Rat)+ (u<|@@↑(( (-a ))))) } ..this.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
this : {U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
this
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
⊢ {U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}
      ·this.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
this : {U | ∃ examples6, u examples6 + u (-examples6) = U} ⊆ {0, u a + u (-a)}
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2 use ( Set.toFinite ( _) ).subset ↑@@this , (Set.ncard_le_ncard$ (((this )) ) ).trans (Set.ncard_pair$ Ne.symm (↑ ( (c)) ) ).leAll goals completed! 🐙
      -- We now proceed to show that f(x) + f(-x) = 0 or k for all x.
      rintro-⟨hz, rfl⟩this.intro
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
      -- We have f(x + f(a)) = f(x) + a or f(f(x) + a) = x + f(a).
      induction b @hz athis.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (hz + u a) = u hz + a
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
      ·this.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (hz + u a) = u hz + a
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)} -- Step "f.": First, consider the case where f(x + f(a)) = f(x) + a.
        /- Step "i.": We have f(-a + f(x + f(a))) = f(-a) + (x + f(a))
            or f(f(-a) + (x + f(a))) = -a + f(x + f(a)). -/
        have:=b (-a)$ hz+u athis.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (hz + u a) = u hz + a
this : u (-a + u (hz + u a)) = u (-a) + (hz + u a) ∨ u (u (-a) + (hz + u a)) = -a + u (hz + u a)
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
        /- Step "ii.": We have f(x + f(x)) = f(x) + x or f(f(x) + x) = x + f(x).
           This simplifies to just f(x + f(x)) = x + f(x).
        -/
        have:=b hz hzthis.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (hz + u a) = u hz + a
this✝ : u (-a + u (hz + u a)) = u (-a) + (hz + u a) ∨ u (u (-a) + (hz + u a)) = -a + u (hz + u a)
this : u (hz + u hz) = u hz + hz ∨ u (u hz + hz) = hz + u hz
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
        /- Step "iii.": Substituting step “f.” into step “i.” and simplifying
            gives f(f(x)) = x + f(a) + f(-a) or f(x + f(a) + f(-a)) = f(x). -/
        simp_all[add_comm]this.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (hz + u a) = a + u hz
this✝ : u (u hz) = hz + u a + u (-a) ∨ u (hz + u a + u (-a)) = u hz
this : u (hz + u hz) = hz + u hz
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        /- Step "iiii.": We have f(-x + f(x + f(x))) = f(-x) + x + f(x) or
           f(f(-x) + x + f(x)) = -x + f(x + f(x)). -/
        have:=b (-hz) (hz+u ↑(hz))this.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (hz + u a) = a + u hz
this✝¹ : u (u hz) = hz + u a + u (-a) ∨ u (hz + u a + u (-a)) = u hz
this✝ : u (hz + u hz) = hz + u hz
this : u (-hz + u (hz + u hz)) = hz + u hz + u (-hz) ∨ u (hz + u hz + u (-hz)) = -hz + u (hz + u hz)
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        /- Substituting step “ii.” into step “iv.”, we have
           f(f(x)) = x + f(-x) + f(x) or f(x + f(-x) + f(x)) = f(x). -/
        simp_all[ add_assoc, C]this.intro.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (hz + u a) = a + u hz
this✝¹ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this✝ : u (hz + u hz) = hz + u hz
this : u (u hz) = hz + (u hz + u (-hz)) ∨ u (hz + (u hz + u (-hz))) = u hz
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        induction thisthis.intro.inl.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
this.intro.inl.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this : u (hz + u hz) = hz + u hz
h✝ : u (hz + (u hz + u (-hz))) = u hz
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        ·this.intro.inl.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a) -- Step "vi.": First, consider the case where f(f(x)) = x + f(-x) + f(x).
          /- Step "vi.1" In this case, step “iii.” simplifies to
             f(-x) + f(x) = f(a) + f(-a)
             or f(x + f(a) + f(-a)) = f(x). In the first case we are done,
             so we focus only on the second case. -/
          simp_allthis.intro.inl.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝ : u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hz
this : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
          /- Step "vi.2": We have
             f(x + f(x + f(a) + f(-a))) = f(x) + x + (f(a) + f(-a)) or
             f(f(x) + x + f(a) + f(-a)) = x + f(x + f(a) + f(-a)). -/
          have:=b hz (hz+(u a+u (-a)))this.intro.inl.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝¹ : u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hz
this✝ : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
this : u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
  u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
          /- Step "vi.3": We have
             f(x + f(a) + f(-a) + f(x + f(a) + f(-a)))
             = x + f(a) + f(-a) + f(x + f(a) + f(-a)). -/
          have:=b (hz+(u a+u (-a)))$ hz+(u a+u (-a))this.intro.inl.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝² : u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hz
this✝¹ : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
this✝ : u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
  u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))
this : u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a))) ∨
  u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
          /- Step "vi.4": Substituting step “vi.1.” into step “vi.2” gives
              f(x +f(x))=f(x)+x+(f(a)+f(-a)) or f(f(x)+x+f(a)+f(-a))=x+f(x).
              Step "vi.5" Substituting step “vi.1.” into step “vi.3.” gives
              f(x+f(a)+f(-a)+f(x))=x+f(a)+f(-a)+f(x).
              Substituting step “vi.5.” into step “vi.4.” and simplifying gives
              f(x +f(x))=f(x)+x+(f(a)+f(-a)) or f(a)+f(-a)=0.
              The former case simplifies via step “ii.” to f(a)+f(-a)=0,
              so in both cases we have a contradiction. -/
          use .inr$ by_contra$ byIsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝² : u hz + u (-hz) = u a + u (-a) ∨ u (hz + (u a + u (-a))) = u hz
this✝¹ : u (hz + u hz) = hz + u hz
h✝ : u (u hz) = hz + (u hz + u (-hz))
this✝ : u (hz + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u hz ∨
  u (hz + (u a + u (-a)) + u hz) = hz + u (hz + (u a + u (-a)))
this : u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a))) ∨
  u (hz + (u a + u (-a)) + u (hz + (u a + u (-a)))) = hz + (u a + u (-a)) + u (hz + (u a + u (-a)))
⊢ ¬u hz + u (-hz) = u a + u (-a) → False Try these:
• aesop
• simp_all only [or_self, imp_false, Decidable.not_not]hintAll goals completed! 🐙
        -- Step "vii." Now, consider the case where f(x + f(-x) + f(x)) = f(x).
        /- Step "vii.1": We have f(x + f(x + f(-x) + f(x))) = f(x) + x + f(-x) + f(x)
            or f(f(x) + x + f(-x) + f(x)) = x + f(x + f(-x) + f(x)). -/
        have:=b hz$ hz+(u hz+u (-hz))this.intro.inl.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (hz + u a) = a + u hz
this✝¹ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this✝ : u (hz + u hz) = hz + u hz
h✝ : u (hz + (u hz + u (-hz))) = u hz
this : u (hz + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u hz ∨
  u (hz + (u hz + u (-hz)) + u hz) = hz + u (hz + (u hz + u (-hz)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        /- Step "vii.2": We have f(f(x + f(-x) + f(x)) + x + f(-x) + f(x)) =
           x + f(-x) + f(x) + f(x + f(-x) + f(x)).
           Step "vii.3": Substituting step “vii.” into step “vii.2.” gives
           f(f(x)+x+f(-x)+f(x))= x+f(-x)+f(x)+f(x).
           Substituting step “vii.” into step “1.” gives
           f(x+f(x))=f(x)+x+f(-x)+f(x) or
           f(f(x)+x+f(-x)+f(x))=x+f(x).
           In the first case we can substitute in step “ii.” and
           simplify to f(-x)+f(x)=0 as desired.
           In the second case we can substitute in step “vii.3” to
           obtain f(-x)+f(x)=0 again as desired. -/
        cases b (hz+(u hz+u (-hz)))$ hz+(u hz+u (-hz))with|_=>this.intro.inl.inr.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
b : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝² : u (hz + u a) = a + u hz
this✝¹ : u (u hz) = hz + (u a + u (-a)) ∨ u (hz + (u a + u (-a))) = u hz
this✝ : u (hz + u hz) = hz + u hz
h✝¹ : u (hz + (u hz + u (-hz))) = u hz
this : u (hz + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u hz ∨
  u (hz + (u hz + u (-hz)) + u hz) = hz + u (hz + (u hz + u (-hz)))
h✝ : u (hz + (u hz + u (-hz)) + u (hz + (u hz + u (-hz)))) = hz + (u hz + u (-hz)) + u (hz + (u hz + u (-hz)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)Try these:
• simp_all only [add_left_inj, self_eq_add_right, add_right_eq_self, or_self, add_zero, true_or]Try these:
• simp_all only [add_left_inj, self_eq_add_right, add_right_eq_self, or_self, add_zero, true_or]hintAll goals completed! 🐙
      -- Step "g.": Now, consider the case where  f(f(x) + a) = x + f(a).
      /- Step "i.": We have f(-x + f(f(x) + a)) = f(-x) + (f(x) + a) or
         f(f(-x) + f(x) + a) = -x + f(f(x) + a). -/
      have:=b (-hz) (u hz+a)this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this : u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
      have:=b$ -athis.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝ : u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)
this : ∀ (y : ℚ), u (-a + u y) = u (-a) + y ∨ u (u (-a) + y) = -a + u y
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
      /- Step "ii." We have f(-a + f(f(x) + a)) = f(-a) + (f(x) + a) or
         f(f(-a) + (f(x) + a)) = -a + f(f(x) + a). -/
      specialize this (u hz+a)this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝ : u (-hz + u (u hz + a)) = u (-hz) + (u hz + a) ∨ u (u (-hz) + (u hz + a)) = -hz + u (u hz + a)
this : u (-a + u (u hz + a)) = u (-a) + (u hz + a) ∨ u (u (-a) + (u hz + a)) = -a + u (u hz + a)
⊢ u hz + u (-hz) ∈ {0, u a + u (-a)}
      /- Step "iii.": Substituting step “g.” into step “i.” gives
         f(f(a)) = f(-x) + (f(x) + a) or f(f(-x) + f(x) + a) = f(a).
         Step "iv.": Substituting step “g.” into step “ii.” gives
         f(-a + x + f(a)) = f(-a) + f(x) + a or
         f(f(-a) + f(x) + a) = -a + x + f(a). -/
      simp_all[ ←add_assoc]this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝ : u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u a
this : u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u a
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      have:=b 0this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝¹ : u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u a
this✝ : u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u a
this : ∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u y
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      have:=bthis.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝² : u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u a
this✝¹ : u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u a
this✝ : ∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u y
this : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      -- Step "v.": We have f(a + f(a)) = a + f(a).
      specialize b a athis.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
a : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
hz : ℚ
h✝ : u (u hz + a) = hz + u a
this✝² : u (u a) = u (-hz) + u hz + a ∨ u (u (-hz) + u hz + a) = u a
this✝¹ : u (-a + hz + u a) = u (-a) + u hz + a ∨ u (u (-a) + u hz + a) = -a + hz + u a
this✝ : ∀ (y : ℚ), u (0 + u y) = u 0 + y ∨ u (u 0 + y) = 0 + u y
this : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
b : u (a + u a) = u a + a ∨ u (u a + a) = a + u a
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      simp_all[add_comm]this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (a + u hz) = hz + u a
this✝¹ : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      /- Step "vi.": We have f(-a + f(a + f(a))) = f(-a) + a + f(a) or
         f(f(-a) + a + f(a)) = -a + f(a + f(a)). -/
      have:=(this<| -a) (↑a + (((u a))): (↑_ :((( _) ) ) )) ..this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (a + u hz) = hz + u a
this✝² : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
this : u (-a + u (a + u a)) = a + u a + u (-a) ∨ u (a + u a + u (-a)) = -a + u (a + u a)
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      /- Step "vii.": Substituting step “v.” into step “vi.” and simplifying gives
         f(f(a)) = a + f(a) + f(-a) or f(a + f(a) + f(-a)) = f(a). -/
      simp_all[add_assoc]this.intro.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝ : u (a + u hz) = hz + u a
this✝² : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
this : u (u a) = a + (u a + u (-a)) ∨ u (a + (u a + u (-a))) = u a
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      cases thisthis.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
this.intro.inr.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (a + (u a + u (-a))) = u a
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      ·this.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a) -- Step "viii.": First, consider the case where f(f(a)) = a + f(a) + f(-a).
        /- Step "viii.1": In this case, step “iii.” simplifies to
            f(a) + f(-a) = f(-x) + f(x) or f(f(-x) + f(x) + a) = f(a).
            In the first case we are done, so we focus only on the second case. -/
        simp_allthis.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
        contrapose! IsAquaesulian_defthis.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : u hz + u (-hz) ≠ 0 ∧ u hz + u (-hz) ≠ u a + u (-a)
⊢ ∃ f,
  (IsAquaesulian f ∧ ∃ x y, f (x + f y) ≠ y + f x ∧ f (y + f x) ≠ x + f y) ∨
    ¬IsAquaesulian f ∧ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
        simp_allthis.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : ¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)
⊢ ∃ f,
  (IsAquaesulian f ∧ ∃ x y, ¬f (x + f y) = y + f x ∧ ¬f (y + f x) = x + f y) ∨
    ¬IsAquaesulian f ∧ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
        exfalsothis.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝¹ : u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u a
this✝ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : ¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)
⊢ False
        /- Step "viii.2": We have
           f(a + f(a + (f(x) + f(-x)))) = a + (f(x) + f(-x)) + f(a) or
           f(a + (f(x) + f(-x)) + f(a)) = a + f(a + (f(x) + f(-x))). -/
        have:=this a (a+(u hz+u ( -hz)))this.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝² : u a + u (-a) = u hz + u (-hz) ∨ u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : ¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)
this : u (a + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u a ∨
  u (a + (u hz + u (-hz)) + u a) = a + u (a + (u hz + u (-hz)))
⊢ False
        simp_all[Ne.symm,Bool]this.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝² : u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : ¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)
this : u (a + (u hz + u (-hz)) + u a) = a + u a
⊢ False
        /- Step "viii.3": We have
           f(a + f(x) + f(-x) + f(a + f(x) + f(-x))) =
           a + f(x) + f(-x) + f(a + f(x) + f(-x)). -/
        have:=‹∀congr_arg G,_› (a+(u hz+u (-hz)))$ a+(u ↑hz+u ↑( -hz) )this.intro.inr.inl
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝³ : u (a + (u hz + u (-hz))) = u a
this✝² : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝¹ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (u a) = a + (u a + u (-a))
IsAquaesulian_def : ¬u hz + u (-hz) = 0 ∧ ¬u hz + u (-hz) = u a + u (-a)
this✝ : u (a + (u hz + u (-hz)) + u a) = a + u a
this : u (a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u (a + (u hz + u (-hz))) ∨
  u (a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))) = a + (u hz + u (-hz)) + u (a + (u hz + u (-hz)))
⊢ False
        /- Step "viii.4": Substituting step “viii.1” into step “viii.3” gives
           f(a + f(x) + f(-x) + f(a))=a + f(x) + f(-x) + f(a).
           The result follows by casework on step “viii.2”; In the first case,
           substituting in step “viii.1” followed by step “v.” gives
           f(x) + f(-x) = 0 as desired, and in the second case,
           substituting in step “viiii.4” followed by step “viii.1” gives
           f(x) + f(-x) = 0 again as desired.
        -/
        simp_allAll goals completed! 🐙
      -- Step "ix.": Now, consider the case where f(a + f(a) + f(-a)) = f(a).
      /- Step "ix.1.": We have f(a + f(a + f(a) + f(-a))) = f(a) + a + f(a) + f(-a)
         or f(f(a) + a + f(a) + f(-a)) = a + f(a + f(a) + f(-a)). -/
      have:=this a (a +(u a+u (-a)))this.intro.inr.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝¹ : u (a + u hz) = hz + u a
this✝² : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝ : u (a + (u a + u (-a))) = u a
this : u (a + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u a ∨ u (a + (u a + u (-a)) + u a) = a + u (a + (u a + u (-a)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)
      /- Step "ix.2.": We have
         f(a + f(a) + f(-a) + f(a + f(a) + f(-a)))
         = a + f(a) + f(-a) + f(a + f(a) + f(-a)).
         Step "ix.3.": Substituting step “ix.” into step “ix.2” gives
         f(a + f(a) + f(-a) +f(a)) = a + f(a) + f(-a) + f(a).
         The result follows by casework on step “ix.1.”: In the first case,
         we can substitute in step “ix.” followed by step “v.” to get f(a)+f(-a)=0,
         and in the second case we can substitute in step “ix.3.”
         followed by step “ix.” to get f(a)+f(-a)=0 again.
         Either way, this contradicts our assumption about a. -/
      cases‹forall Jd S,_› (a+(u a+u (-a))) ( a + (u a +u ↑(-a)))with| _ =>this.intro.inr.inr.inr
IsAquaesulian : (ℚ → ℚ) → Prop
u : ℚ → ℚ
a : ℚ
hz : ℚ
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = y + f x ∨ f (y + f x) = x + f y
j : u 0 = 0
c : ¬u a + u (-a) = 0
h✝² : u (a + u hz) = hz + u a
this✝² : u (u a) = a + (u hz + u (-hz)) ∨ u (a + (u hz + u (-hz))) = u a
this✝¹ : u (u a + (hz + -a)) = a + (u hz + u (-a)) ∨ u (a + (u hz + u (-a))) = u a + (hz + -a)
this✝ : ∀ (x y : ℚ), u (x + u y) = y + u x ∨ u (y + u x) = x + u y
b : u (a + u a) = a + u a
h✝¹ : u (a + (u a + u (-a))) = u a
this : u (a + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u a ∨ u (a + (u a + u (-a)) + u a) = a + u (a + (u a + u (-a)))
h✝ : u (a + (u a + u (-a)) + u (a + (u a + u (-a)))) = a + (u a + u (-a)) + u (a + (u a + u (-a)))
⊢ u hz + u (-hz) = 0 ∨ u hz + u (-hz) = u a + u (-a)Try these:
• simp_all only [add_left_inj, self_eq_add_right, false_or]Try these:
• simp_all only [add_left_inj, self_eq_add_right, false_or]hintAll goals completed! 🐙
    /- Now let f be an aquaesulian function with f(0) ≠ 0.
       We will derive a contradiction. -/
    simp_allrefine_1.refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : ¬u 0 = 0
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2
    /- We have:
       P(0, 0) -> f(f(0)) = f(0),
       P(f(0), f(0)) -> f(f(0) + f(f(0))) = f(0) + f(f(0)) ->
       f(2f(0)) = 2f(0),
       P(0, f(0)) -> f(f(f(0))) = 2f(0) or f(2f(0)) = f(f(0)) ->
       f(0) = 2f(0) or f(2f(0)) = f(0) -> f(0) = 2f(0) or 2f(0) = f(0),
       so f(0) = 0 as desired. -/
    cases b 0 0with|_=>refine_1.refine_2.inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : ¬u 0 = 0
h✝ : u (u 0 + 0) = 0 + u 0
⊢ {x | ∃ r, u r + u (-r) = x}.Finite ∧ {x | ∃ r, u r + u (-r) = x}.ncard ≤ 2exact absurd (b 0$ (0+(1 *(@(u ↑.((0) )))))^ 01: ↑ ((_)) ) (id$ (byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : ¬u 0 = 0
h✝ : u (u 0 + 0) = 0 + u 0
⊢ ¬(u (0 + u ((0 + 1 * u 0) ^ 1)) = u 0 + (0 + 1 * u 0) ^ 1 ∨ u (u 0 + (0 + 1 * u 0) ^ 1) = 0 + u ((0 + 1 * u 0) ^ 1))(cases ( b (u 0) ( (u 0)))with|_ =>inr
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
u : ℚ → ℚ
b : ∀ (x y : ℚ), u (x + u y) = u x + y ∨ u (u x + y) = x + u y
j : ¬u 0 = 0
h✝¹ : u (u 0 + 0) = 0 + u 0
h✝ : u (u (u 0) + u 0) = u 0 + u (u 0)
⊢ ¬(u (0 + u ((0 + 1 * u 0) ^ 1)) = u 0 + (0 + 1 * u 0) ^ 1 ∨ u (u 0 + (0 + 1 * u 0) ^ 1) = 0 + u ((0 + 1 * u 0) ^ 1)) continuityAll goals completed! 🐙)))
  rintro K Vrefine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : K ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}
⊢ 2 ≤ K
  -- Now let f(x) = -x + 2⌈x⌉. We claim that f is aquaesulian.
  specialize V $ λ N=>-N+2 *Int.ceil Nrefine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ 2 ≤ K
  specialize( V $ (IsAquaesulian_def _).mpr _)refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ),
  -(x + (-y + 2 * ↑⌈y⌉)) + 2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y ∨
    -(-x + 2 * ↑⌈x⌉ + y) + 2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉)
refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧ ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ 2 ≤ K
  ·refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ),
  -(x + (-y + 2 * ↑⌈y⌉)) + 2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y ∨
    -(-x + 2 * ↑⌈x⌉ + y) + 2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉) simp_rw [ ←eq_sub_iff_add_eq'refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ),
  2 * ↑⌈x + (-y + 2 * ↑⌈y⌉)⌉ = -x + 2 * ↑⌈x⌉ + y - -(x + (-y + 2 * ↑⌈y⌉)) ∨
    2 * ↑⌈-x + 2 * ↑⌈x⌉ + y⌉ = x + (-y + 2 * ↑⌈y⌉) - -(-x + 2 * ↑⌈x⌉ + y)]
    /- The functional equation simplifies to
       ⌈x - y + ⌈y⌉ * 2⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2 or
       ⌈-x + y + ⌈x⌉ * 2⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2. -/
    Try this: ring_nfringrefine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ), ↑⌈x - y + ↑⌈y⌉ * 2⌉ * 2 = ↑⌈y⌉ * 2 + ↑⌈x⌉ * 2 ∨ ↑⌈-x + y + ↑⌈x⌉ * 2⌉ * 2 = ↑⌈y⌉ * 2 + ↑⌈x⌉ * 2
    use mod_cast@?_refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ), ⌈x - y + ↑(⌈y⌉ * 2)⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2 ∨ ⌈-x + y + ↑(⌈x⌉ * 2)⌉ * 2 = ⌈y⌉ * 2 + ⌈x⌉ * 2
    /- Which is equivalent to:
       (A) ⌈y⌉ + ⌈x⌉ - 1 < x - y + ⌈y⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ or
       (B) ⌈y⌉ + ⌈x⌉ - 1 < -x + y + ⌈x⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ -/
    norm_num[<-add_mul,Int.ceil_eq_iff]refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : (IsAquaesulian fun N => -N + 2 * ↑⌈N⌉) →
  {x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.Finite ∧
    ↑{x | ∃ r, -r + 2 * ↑⌈r⌉ + (- -r + 2 * ↑⌈-r⌉) = x}.ncard ≤ K
⊢ ∀ (x y : ℚ),
  ↑⌈y⌉ + ↑⌈x⌉ - 1 < x - y + ↑⌈y⌉ * 2 ∧ x - y + ↑⌈y⌉ * 2 ≤ ↑⌈y⌉ + ↑⌈x⌉ ∨
    ↑⌈y⌉ + ↑⌈x⌉ - 1 < -x + y + ↑⌈x⌉ * 2 ∧ -x + y + ↑⌈x⌉ * 2 ≤ ↑⌈y⌉ + ↑⌈x⌉
    useλc K=>(em _).imp (⟨byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ IsLeast
  {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 linarith[Int.ceil_lt_add_one c,Int.le_ceil K],.⟩) (byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ IsLeast
  {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 repeat use byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
⊢ IsLeast
  {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2 linarith[.,Int.le_ceil c,or,Int.ceil_lt_add_one$ K])
    /- If x - y + ⌈y⌉ * 2 ≤ ⌈y⌉ + ⌈x⌉ then we have the desired result (A)
       since ⌈y⌉ < y + 1.
       Otherwise, we have ⌈y⌉ + ⌈x⌉ < x - y + ⌈y⌉ * 2 which we negate and
       add ⌈x⌉ * 2 + ⌈y⌉ * 2 to get -x + y + ⌈x⌉ * 2 < ⌈y⌉ + ⌈x⌉,
       from which we get the desired result (B) since ⌈x⌉ < x + 1. -/
  simp_all[Int.ceil_neg, ←add_assoc]refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
⊢ 2 ≤ K
  suffices:2<=V.1.toFinset.cardrefine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
this : 2 ≤ ⋯.toFinset.card
⊢ 2 ≤ K
this
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
⊢ 2 ≤ ⋯.toFinset.card
  ·refine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
this : 2 ≤ ⋯.toFinset.card
⊢ 2 ≤ K let M:=V.1.toFinsetrefine_2
IsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
this : 2 ≤ ⋯.toFinset.card
M : Finset ℚ := ⋯.toFinset
⊢ 2 ≤ K
    norm_num[this,V.2.trans',(Set.ext$ byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
this : 2 ≤ ⋯.toFinset.card
M : Finset ℚ := ⋯.toFinset
⊢ ∀ (x : ℚ), x ∈ {x | ∃ t, 2 * ↑⌈t⌉ + -(2 * ↑⌊t⌋) = x} ↔ x ∈ ↑M simp_all[M]All goals completed! 🐙 : {x :Rat|∃t:Rat, (↑2 ) * ( ⌈ t ⌉:(ℚ ) ) .. + (- (2 *⌊(t)⌋)) = ↑x} = M)]
  /- Finally, we have f(-1) + f(1) = 0 and f(1/2) = f(-1/2) = 2
     as two distinct values of f. Thus, c = 2 is tight as desired. -/
  use Finset.one_lt_card.2$ byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
⊢ ∃ a ∈ ⋯.toFinset, ∃ b ∈ ⋯.toFinset, a ≠ b exists@0,V.1.mem_toFinset.2 (byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
⊢ 0 ∈ {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x} exists-1All goals completed! 🐙),2,V.1.mem_toFinset.2 (byIsAquaesulian : (ℚ → ℚ) → Prop
IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y
K : ℤ
V : {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.Finite ∧ ↑{x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x}.ncard ≤ K
⊢ 2 ∈ {x | ∃ r, 2 * ↑⌈r⌉ + -(2 * ↑⌊r⌋) = x} exists 1/2All goals completed! 🐙)

The following command shows which axioms the proof relies upon:

'imo_2024_p6' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms imo_2024_p6

'imo_2024_p6' depends on axioms: [propext, Classical.choice, Quot.sound]

These are the standard built in axioms.