548.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/548
[BrDo96] Brandt, Stephan and Dobson, Edward, The Erdős-Sós conjecture for graphs of girth {$5$}. Discrete Math. (1996), 411-414.
[Er78] Erdős, Paul, Problems and results in combinatorial analysis and combinatorial number theory. Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1978) (1978), 29-40.
[ErGa59] Erdős, P. and Gallai, T., On maximal paths and circuits of graphs. Acta Math. Acad. Sci. Hungar. (1959), 337-356 (unbound insert).
[SaWo97] Saclé, Jean-François and Woźniak, Mariusz, The Erdős-Sós conjecture for graphs without {$C_4$}. J. Combin. Theory Ser. B (1997), 367-372.
[WLL00] Wang, Min and Li, Guo-jun and Liu, Ai-de, A result of Erdős-Sós conjecture. Ars Combin. (2000), 123-127.
[YiLi04] Yin, Jian-hua and Li, Jiong-sheng, The Erdős-Sós conjecture for graphs whose complements contain no {$C_4$}. Acta Math. Appl. Sin. Engl. Ser. (2004), 397-400.

Imports (1)

theorem Erdos548.erdos_548 sorry line 51 source
depends on sorry what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, SimpleGraph, Fin, Rat, HMul.hMul, HDiv.hDiv, HSub.hSub, Set.ncard, Sym2, SimpleGraph.edgeSet, SimpleGraph.IsTree, SimpleGraph.IsContained
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.