},
{ intro h,

have := @quasi_adjoint C D P,
simp [←pi_1_etalisation, this, h],
refl

}
end

Figure 20: Example of infilling in the Lean 3 programming language on a fictional algebraic geometry problem.
The mathematical terms “quasi-prefunctoid”, “precategoroid” and “etalisation” do not exist and were invented
to make sure the model did not memorize. The model uses a plausible parametrization of “etalisations” of P
via morphisms f of the underlying “precategoroids” and invents a notation for the induced “etalisation” of P.
The ∀ quantification and the use of the variable name f are both suggested by the context. It also correctly
expresses “1-connectedness” via the π1 functor present in the context.
CodeLlama2