Compfiles/Usa2022P3.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2022, Problem 3

Let ℝ+ be the set of all positive real numbers. Find all functions ℝ+ → ℝ+ such that for all x, y ∈ ℝ+ we have

f(x) = f(f(f(x)) + y) + f(xf(y))f(x+y).

Imports (5)
Imported by 1 file
  1. abbrev Usa2022P3.PosReal line 31 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Proof uses: Subtype, Real, LT.lt, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. lemma Usa2022P3.PosReal.lt_add line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Usa2022P3.PosReal, LT.lt, Real, OfNat.ofNat, HAdd.hAdd

    Proof uses: Iff.mpr, Subtype, Subtype.mk, Subtype.property, Subtype.mk_lt_mk, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring and 35 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  3. theorem Usa2022P3.PosReal.coe_mul line 42 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Usa2022P3.PosReal, Eq, Real, LT.lt, OfNat.ofNat, HMul.hMul

    Proof uses: rfl

    19 instances, coercions and auxiliary constants left out.

  4. theorem Usa2022P3.PosReal.coe_add line 45 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Usa2022P3.PosReal, Eq, Real, LT.lt, OfNat.ofNat, HAdd.hAdd

    Proof uses: rfl

    41 instances, coercions and auxiliary constants left out.

  5. theorem Usa2022P3.PosReal.coe_div line 48 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Usa2022P3.PosReal, Eq, Real, LT.lt, OfNat.ofNat, HDiv.hDiv

    Proof uses: rfl

    25 instances, coercions and auxiliary constants left out.

  6. determine Usa2022P3.solution_set line 52 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Usa2022P3.PosReal

    Proof uses: Set.ofPred, Exists, Eq, HDiv.hDiv, Real

    8 instances, coercions and auxiliary constants left out.

  7. problem Usa2022P3.usa2022_p3 line 55 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Usa2022P3.PosReal, Iff, Membership.mem, Set, Usa2022P3.solution_set, Eq, HAdd.hAdd, Real, HMul.hMul

    Proof uses: Iff.intro, HDiv.hDiv, LT.lt, OfNat.ofNat, Subtype.mk, Iff.mpr, Subtype, Inv.inv, Subtype.mk_eq_mk, Eq.mpr, id, congrArg, congrFun', div_div_cancel, of_eq_true, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq and 193 more

    228 instances, coercions and auxiliary constants left out.

    Tactic trace: 170 steps

    Open to load the checked before-and-after goal states.