`Compfiles/Imo2017P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

22 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2017, Problem 2

Find all functions f : ℝ → ℝ that satisfy

∀ x,y ∈ ℝ, f(f(x)f(y)) + f(x + y) = f(xy).

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2017P2.good line 46 source
no axioms what this means
Statement uses: Ring
Proof uses: Eq, HAdd.hAdd, HMul.hMul
6 instances, coercions and auxiliary constants left out.
theorem Imo2017P2.good_zero line 51 source
no axioms what this means
Statement uses: Ring, Imo2017P2.good, OfNat.ofNat
Proof uses: add_zero
13 instances, coercions and auxiliary constants left out.
theorem Imo2017P2.good_one_sub line 54 source
standard axioms: propext what this means
Statement uses: Ring, Imo2017P2.good, HSub.hSub, OfNat.ofNat
Proof uses: Eq.mpr, Eq, HAdd.hAdd, HMul.hMul, Neg.neg, id, congr, congrArg, Eq.trans, sub_eq_add_neg, mul_add, mul_one, mul_neg, add_mul, one_mul, neg_mul
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_neg line 65 source
standard axioms: propext what this means
Statement uses: Ring, Imo2017P2.good, Neg.neg
Proof uses: Eq.mpr, Eq, HAdd.hAdd, HMul.hMul, id, congrArg, Pi.neg_apply, neg_mul_neg, Eq.symm, neg_add, Eq.refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_special_equality (1) line 70 source
Source documentation
(1)

standard axioms: propext what this means
Statement uses: Ring, Imo2017P2.good, Eq, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, add_eq_right, add_one_mul, mul_add_one, add_comm, Eq.refl
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem good_special_equality {x y : R} (h0 : x * y = 1) :
    f (f (x + 1) * f (y + 1)) = 0 := by
…
```
Mentions: f
theorem Imo2017P2.good_map_map_zero_sq line 74 source
standard axioms: propext what this means
Statement uses: Ring, Imo2017P2.good, Eq, HPow.hPow, Nat, OfNat.ofNat
Proof uses: HMul.hMul, Neg.neg, Eq.mpr, id, congrArg, neg_mul_neg, mul_one, Eq.refl, HAdd.hAdd, Imo2017P2.good_special_equality, Eq.mp, Eq.symm, sq, neg_add_cancel
54 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_eq_of_inj line 79 source
standard axioms: Quot.sound, propext what this means
Statement uses: Ring, Imo2017P2.good, Eq, OfNat.ofNat, Function.Injective, HSub.hSub
Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, HMul.hMul, MulZeroClass.mul_zero, add_zero, mul_one, Eq.refl, funext, propext, eq_sub_iff_add_eq', add_left_inj, add_comm
51 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_map_eq_zero line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Ne, OfNat.ofNat, Eq
Proof uses: Not.imp_symm, Not, HMul.hMul, HAdd.hAdd, HSub.hSub, Inv.inv, Imo2017P2.good_special_equality, mul_inv_cancel₀, sub_ne_zero_of_ne, funext, Eq.mpr, id, congrArg, Pi.zero_apply, Eq.symm, Eq.mp, MulZeroClass.zero_mul, sub_add_cancel, MulZeroClass.mul_zero, zero_add and 2 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_map_zero_sq line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Ne, OfNat.ofNat, Eq, HPow.hPow, Nat
Proof uses: Imo2017P2.good_map_eq_zero, Imo2017P2.good_map_map_zero_sq
26 instances, coercions and auxiliary constants left out.
theorem Imo2017P2.good_map_zero line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Ne, OfNat.ofNat, Or, Eq, Neg.neg
Proof uses: Iff.mp, HPow.hPow, Nat, sq_eq_one_iff, Imo2017P2.good_map_zero_sq
39 instances, coercions and auxiliary constants left out.
theorem Imo2017P2.good_map_one line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat
Proof uses: Or.elim, Ne, eq_or_ne, congr_fun, Eq.rec, HPow.hPow, Nat, Imo2017P2.good_map_map_zero_sq, Imo2017P2.good_map_zero_sq
24 instances, coercions and auxiliary constants left out.
theorem Imo2017P2.good_map_eq_zero_iff (2) line 119 source
Source documentation
(2)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat, Iff
Proof uses: Iff.intro, Imo2017P2.good_map_eq_zero, zero_ne_one, Eq.mp, congrArg, Eq.rec, congr_arg, Imo2017P2.good_map_one
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem good_map_eq_zero_iff (h0 : f 0 = 1) (c : D) : f c = 0 ↔ c = 1 :=
…
```
Mentions: f
theorem Imo2017P2.good_shift (3) line 125 source
Source documentation
(3)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat, HAdd.hAdd
Proof uses: HMul.hMul, Eq.mp, congrArg, mul_one, add_comm, MulZeroClass.mul_zero, Imo2017P2.good_map_one
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem good_shift (h0 : f 0 = 1) (x : D) : f (x + 1) + 1 = f x := by
…
```
Mentions: f
theorem Imo2017P2.good_shift2 line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat, HSub.hSub, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Imo2017P2.good_shift, sub_add_cancel, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.good_map_add_one_eq_zero_iff line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat, Iff, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, propext, Imo2017P2.good_map_eq_zero_iff, add_eq_right, Iff.rfl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Imo2017P2.solution_of_map_zero_eq_one_imp_injective The general framework; reducing to injectivity line 139 source
Source documentation
The general framework; reducing to injectivity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Imo2017P2.good, Eq, OfNat.ofNat, Function.Injective, Iff, Or, HSub.hSub, Neg.neg
Proof uses: Iff.intro, Eq.mpr, Not, id, congrArg, propext, Classical.or_iff_not_imp_left, Or.imp, Imo2017P2.good_map_zero, Imo2017P2.good_eq_of_inj, Eq.symm, neg_eq_iff_eq_neg, Imo2017P2.good_neg, Eq.mp, Imo2017P2.good_zero, Imo2017P2.good_one_sub
53 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem solution_of_map_zero_eq_one_imp_injective
    (h : ∀ f : D → D, good f → f 0 = 1 → Injective f) {f : D → D} :
    good f ↔ f = 0 ∨ f = (1 - ·) ∨ f = -(1 - ·) := by
…
```
Mentions: h, f, Imo2017P2.good
theorem Imo2017P2.case1_injective Injectivity for char(D) ≠ 2, D a division ring line 155 source
Source documentation
Injectivity for char(D) ≠ 2, D a division ring

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DivisionRing, Ne, OfNat.ofNat, Nat, Imo2017P2.good, Eq, Function.Injective
Proof uses: HSub.hSub, HAdd.hAdd, Imo2017P2.good_shift2, HMul.hMul, Neg.neg, Eq.mpr, id, congrArg, add_assoc, Eq.symm, neg_one_mul, congr_arg₂, zero_sub, one_add_one_eq_two, Eq.refl, add_comm, neg_add_eq_sub, Eq.mp, propext, Imo2017P2.good_map_add_one_eq_zero_iff and 13 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem case1_injective (h : (2 : D) ≠ 0)
    {f : D → D} (h0 : good f) (h1 : f 0 = 1) : Injective f := by
…
```
Mentions: h, f, Imo2017P2.good
theorem Imo2017P2.case2_injective Injectivity for char(F) = 2 line 185 source
Source documentation
Injectivity for char(F) = 2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Eq, OfNat.ofNat, Nat, Imo2017P2.good, Function.Injective
Proof uses: HAdd.hAdd, Imo2017P2.good_shift, Ne, HSub.hSub, HMul.hMul, Inv.inv, Eq.mpr, id, congrArg, Imo2017P2.good_shift2, Eq.symm, add_assoc, Imo2017P2.good_special_equality, mul_inv_cancel₀, zero_add, add_right_comm, Eq.refl, Iff, Imo2017P2.good_map_add_one_eq_zero_iff, Or and 69 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
theorem case2_injective [Field F] (h : (2 : F) = 0)
    {f : F → F} (h0 : good f) (h1 : f 0 = 1) : Injective f := by
…
```
Mentions: h, f, Imo2017P2.good
theorem Imo2017P2.map_zero_eq_one_imp_injective Injectivity line 224 source
Source documentation
Injectivity

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Imo2017P2.good, Eq, OfNat.ofNat, Function.Injective
Proof uses: Or.elim, Ne, Nat, ne_or_eq, Imo2017P2.case1_injective, Imo2017P2.case2_injective
29 instances, coercions and auxiliary constants left out.
```
theorem map_zero_eq_one_imp_injective [Field F] :
    ∀ f : F → F, good f → f 0 = 1 → Injective f :=
…
```
Mentions: f, Imo2017P2.good
theorem Imo2017P2.final_solution Final solution line 229 source
Source documentation
Final solution

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Iff, Imo2017P2.good, Or, Eq, OfNat.ofNat, Sub.sub, Neg.neg, HSub.hSub
Proof uses: Imo2017P2.solution_of_map_zero_eq_one_imp_injective, Imo2017P2.map_zero_eq_one_imp_injective
24 instances, coercions and auxiliary constants left out.
```
theorem final_solution [Field F] {f : F → F} :
    good f ↔ f = 0 ∨ f = Sub.sub 1 ∨ f = fun x ↦ -(1 - x) :=
…
```
Mentions: f, Imo2017P2.good
determine Imo2017P2.solution_set line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Insert.insert, OfNat.ofNat, HSub.hSub, Singleton.singleton
8 instances, coercions and auxiliary constants left out.
problem Imo2017P2.imo2017_p2 line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Set, Imo2017P2.solution_set, Eq, HAdd.hAdd, HMul.hMul
Proof uses: Imo2017P2.good, Or, OfNat.ofNat, Sub.sub, Neg.neg, HSub.hSub, Imo2017P2.final_solution, Iff.intro, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Eq.symm and 55 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.