Compfiles/Imo1979P6.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1979, Problem 6

Let $A$ and $E$ be opposite vertices of an octagon. A frog starts at vertex $A.$ From any vertex except $E$ it jumps to one of the two adjacent vertices. When it reaches $E$ it stops. Let $a_n$ be the number of distinct paths of exactly $n$ jumps ending at $E$. Prove that: \[a_{2n-1}=0, \quad a_{2n}={(2+\sqrt2)^{n-1} - (2-\sqrt2)^{n-1} \over\sqrt2}.\]

Imports (2)
Imported by 1 file
  1. abbrev Imo1979P6.Octagon line 30 source

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

    Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat

    Proof uses: SimpleGraph.cycleGraph

    2 instances, coercions and auxiliary constants left out.

  2. abbrev Imo1979P6.A line 31 source

    standard axioms: propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat

    4 instances, coercions and auxiliary constants left out.

  3. abbrev Imo1979P6.E line 32 source

    standard axioms: propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat

    4 instances, coercions and auxiliary constants left out.

  4. def Imo1979P6.isTerminalWalk line 34 source

    no axioms what this means

    Statement uses: SimpleGraph, SimpleGraph.Walk

    Proof uses: Not, Membership.mem, List, List.dropLast, SimpleGraph.Walk.support

    1 instances, coercions and auxiliary constants left out.

  5. def Imo1979P6.a line 36 source

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

    Statement uses: Nat

    Proof uses: Set.ncard, SimpleGraph.Walk, Fin, OfNat.ofNat, Imo1979P6.Octagon, Imo1979P6.A, Imo1979P6.E, Set.ofPred, And, Imo1979P6.isTerminalWalk, Eq, SimpleGraph.Walk.length

    1 instances, coercions and auxiliary constants left out.

  6. instance Imo1979P6.instFintypeAnd line 40 source

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

    Statement uses: DecidableEq, Fintype, Subtype, DecidablePred, And

    Proof uses: Fintype.mk, Finset.image, Membership.mem, Finset, Finset.filter, Fintype.elems, Subtype.mk, Finset.attach

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  7. instance Imo1979P6.Set.instFintypeElemOfSubtype line 52 source

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

    Statement uses: Fintype, Subtype, Set.ofPred

    Proof uses: Fintype.mk, Fintype.elems

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  8. theorem Imo1979P6.Walk.append_getVert line 62 source

    standard axioms: propext what this means

    Statement uses: SimpleGraph, SimpleGraph.Walk, Eq, SimpleGraph.Walk.getVert, SimpleGraph.Walk.append, SimpleGraph.Walk.length

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, LT.lt, Nat, HSub.hSub, SimpleGraph.Walk.getVert_append, ite_eq_right_of_eq_false, OfNat.ofNat, tsub_self, SimpleGraph.Walk.getVert_zero, eq_self

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  9. theorem Imo1979P6.Walk.take_append line 67 source

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

    Statement uses: SimpleGraph, SimpleGraph.Walk, Eq, SimpleGraph.Walk.getVert, SimpleGraph.Walk.append, SimpleGraph.Walk.length, SimpleGraph.Walk.take, SimpleGraph.Walk.copy, rfl

    Proof uses: SimpleGraph.Walk.ext_support, Eq.mpr, List, SimpleGraph.Walk.support, List.take, HAdd.hAdd, Nat, OfNat.ofNat, id, congrArg, SimpleGraph.Walk.support_take, HAppend.hAppend, List.tail, SimpleGraph.Walk.support_append, of_eq_true, Eq.trans, True, congr, List.take_left', List.length and 4 more

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  10. theorem Imo1979P6.Walk.drop_append_of_length_eq line 75 source

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

    Statement uses: SimpleGraph, SimpleGraph.Walk, Eq, SimpleGraph.Walk.getVert, SimpleGraph.Walk.append, SimpleGraph.Walk.length, SimpleGraph.Walk.drop, SimpleGraph.Walk.copy, rfl

    Proof uses: SimpleGraph.Walk.ext_support, Eq.mpr, List, SimpleGraph.Walk.support, List.drop, Min.min, Nat, id, congrArg, SimpleGraph.Walk.drop_support_eq_support_drop_min, HAppend.hAppend, List.dropLast, SimpleGraph.Walk.support_append_eq_support_dropLast_append, of_eq_true, Eq.trans, True, congr, congrFun', HAdd.hAdd, SimpleGraph.Walk.length_append and 11 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  11. theorem Imo1979P6.isTerminalWalk_copy line 83 source

    standard axioms: propext what this means

    Statement uses: SimpleGraph, Eq, SimpleGraph.Walk, Imo1979P6.isTerminalWalk, SimpleGraph.Walk.copy

    Proof uses: id, Not, Membership.mem, List, List.dropLast, SimpleGraph.Walk.support, of_eq_true, Eq.trans, False, True, congrArg, congr, SimpleGraph.Walk.support_copy, Eq.symm, eq_false, not_false_eq_true

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  12. theorem Imo1979P6.isTerminalWalk_map line 88 source

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

    Statement uses: SimpleGraph, SimpleGraph.Embedding, SimpleGraph.Walk, Imo1979P6.isTerminalWalk, SimpleGraph.Hom, SimpleGraph.Adj, SimpleGraph.Embedding.toHom, SimpleGraph.Walk.map

    Proof uses: id, Not, Membership.mem, List, List.dropLast, SimpleGraph.Walk.support, Eq.mpr, List.map, RelEmbedding, Eq, congrArg, congrFun', SimpleGraph.Walk.support_map, Mathlib.Tactic.Contrapose.contrapose₄, List.take, HSub.hSub, Nat, List.length, OfNat.ofNat, List.dropLast_eq_take and 16 more

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  13. theorem Imo1979P6.isTerminalWalk_of_isSubwalk line 99 source

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

    Statement uses: SimpleGraph, SimpleGraph.Walk, Imo1979P6.isTerminalWalk, SimpleGraph.Walk.IsSubwalk

    Proof uses: id, Exists, List, Eq, HAppend.hAppend, SimpleGraph.Walk.support, Not, Membership.mem, List.dropLast, Eq.mp, List.IsInfix, congrArg, List.IsInfix.eq_1, propext, SimpleGraph.Walk.isSubwalk_iff_support_isInfix, Mathlib.Tactic.Contrapose.contrapose₄, ite, Bool, List.isEmpty, Bool.true and 20 more

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  14. instance Imo1979P6.instDecidableIsTerminalWalk line 113 source

    standard axioms: propext what this means

    Statement uses: DecidableEq, SimpleGraph, DecidablePred, SimpleGraph.Walk, Imo1979P6.isTerminalWalk

    Proof uses: id, Decidable, inferInstance, Not, Membership.mem, List, List.dropLast, SimpleGraph.Walk.support

    5 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  15. abbrev Imo1979P6.C line 118 source

    standard axioms: propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat

    4 instances, coercions and auxiliary constants left out.

  16. abbrev Imo1979P6.G line 119 source

    standard axioms: propext what this means

    Statement uses: Fin, OfNat.ofNat, Nat

    4 instances, coercions and auxiliary constants left out.

  17. def Imo1979P6.b line 121 source

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

    Statement uses: Nat

    Proof uses: Set.ncard, SimpleGraph.Walk, Fin, OfNat.ofNat, Imo1979P6.Octagon, Imo1979P6.C, Imo1979P6.E, Set.ofPred, And, Imo1979P6.isTerminalWalk, Eq, SimpleGraph.Walk.length

    1 instances, coercions and auxiliary constants left out.

  18. def Imo1979P6.Octagon.mirror line 123 source

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

    Statement uses: SimpleGraph.Iso, Fin, OfNat.ofNat, Nat, Imo1979P6.Octagon

    Proof uses: RelIso.mk, SimpleGraph.Adj, Equiv.mk, Neg.neg

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  19. def Imo1979P6.C_G_symm line 134 source

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

    Statement uses: Nat, Equiv, Subtype, SimpleGraph.Walk, Fin, OfNat.ofNat, Imo1979P6.Octagon, Imo1979P6.C, Imo1979P6.E, And, Imo1979P6.isTerminalWalk, Eq, SimpleGraph.Walk.length, Imo1979P6.G

    Proof uses: Equiv.mk, Imo1979P6.C_G_symm.match_1, Subtype.mk, SimpleGraph.Walk.copy, SimpleGraph.Hom, SimpleGraph.Adj, SimpleGraph.Iso.toHom, Imo1979P6.Octagon.mirror, SimpleGraph.Walk.map, Imo1979P6.C_G_symm.match_2

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

  20. def Imo1979P6.isTerminalWalk_length_cons_equiv line 165 source

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

    Statement uses: SimpleGraph, Nat, LT.lt, OfNat.ofNat, Equiv, Subtype, SimpleGraph.Walk, And, Imo1979P6.isTerminalWalk, Eq, SimpleGraph.Walk.length, HAdd.hAdd, Sigma, Prod, Not, Membership.mem, List, SimpleGraph.Walk.support

    Proof uses: Equiv.mk, Imo1979P6.isTerminalWalk_length_cons_equiv.match_1, Sigma.mk, SimpleGraph.Walk.getVert, Prod.mk, Subtype.mk, SimpleGraph.Walk.take, SimpleGraph.Walk.drop, Imo1979P6.isTerminalWalk_length_cons_equiv.match_2, SimpleGraph.Walk.append

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

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

  21. theorem Imo1979P6.a_b_recurrence_1 line 213 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo1979P6.a, HAdd.hAdd, HMul.hMul, Imo1979P6.b

    Proof uses: Fin, Fintype.card, Subtype, SimpleGraph.Walk, Imo1979P6.Octagon, Imo1979P6.A, And, Not, Membership.mem, List, SimpleGraph.Walk.support, Imo1979P6.E, SimpleGraph.Walk.length, Set, SimpleGraph.neighborSet, Ord.compare, Unit, of_decide_eq_true, id, Bool and 73 more

    88 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

  22. theorem Imo1979P6.a_b_recurrence_2 line 244 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo1979P6.b, HAdd.hAdd, Imo1979P6.a, HMul.hMul

    Proof uses: Fin, Fintype.card, Subtype, SimpleGraph.Walk, Imo1979P6.Octagon, Imo1979P6.C, And, Not, Membership.mem, List, SimpleGraph.Walk.support, Imo1979P6.E, SimpleGraph.Walk.length, Set, SimpleGraph.neighborSet, Ord.compare, Unit, of_decide_eq_true, id, Bool and 69 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  23. theorem Imo1979P6.a_even line 274 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Real, Imo1979P6.a, HMul.hMul, HDiv.hDiv, HSub.hSub, HPow.hPow, HAdd.hAdd, Real.sqrt

    Proof uses: And, Imo1979P6.b, Nat.le_induction, Nat.succ, LE.le, id, Set.ncard, SimpleGraph.Walk, Fin, Imo1979P6.Octagon, Imo1979P6.A, Imo1979P6.E, Set.ofPred, Imo1979P6.isTerminalWalk, SimpleGraph.Walk.length, Eq.mpr, Imo1979P6.C, congr, congrArg, congrFun' and 131 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  24. theorem Imo1979P6.walk_even line 302 source

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

    Statement uses: SimpleGraph.Walk, Fin, OfNat.ofNat, Nat, Imo1979P6.Octagon, Imo1979P6.A, Imo1979P6.E, Even, SimpleGraph.Walk.length

    Proof uses: SimpleGraph.Coloring, SimpleGraph.cycleGraph, Bool, SimpleGraph.cycleGraph.bicoloring_of_even, of_eq_true, Eq.trans, Eq, HMod.hMod, True, eq_self, Eq.mpr, Iff, SimpleGraph.Adj, SimpleGraph.completeGraph, Bool.true, id, congrArg, propext, SimpleGraph.Coloring.even_length_iff_congr, of_decide_eq_true and 2 more

    11 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  25. theorem Imo1979P6.a_odd line 307 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo1979P6.a, HSub.hSub, HMul.hMul

    Proof uses: id, Eq.mpr, Set.ncard, SimpleGraph.Walk, Fin, Imo1979P6.Octagon, Imo1979P6.A, Imo1979P6.E, Set.ofPred, And, Imo1979P6.isTerminalWalk, SimpleGraph.Walk.length, Finset.card, Set.toFinset, Membership.mem, Set, SimpleGraph.neighborSet, congrArg, Set.ncard_eq_toFinset_card', Finset and 6 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  26. problem Imo1979P6.imo1979_p6 line 318 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, And, Eq, Imo1979P6.a, HSub.hSub, HMul.hMul, Real, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Real.sqrt

    Proof uses: And.intro, Imo1979P6.a_odd, Imo1979P6.a_even

    42 instances, coercions and auxiliary constants left out.