@AsafKaragila If it makes you feel better we can call it "Lebesgue finitely additive measure." Doesn't have the same ring though.

Yes, by compactness of the unit interval, which is also choiceless. In any case, see Foreman and Wehrung's "The Hahn-Banach Theorem implies the existence of a non-Lebesgue measurable set" for a full discussion on choiceless Lebesgue measure.

Lebesgue measure makes sense in choiceless contexts, but it is only finitely additive.

In this context, $X \subset [0, 1]$ is measurable if $\lambda^*(X)+\lambda^*([0,1] \setminus X) = 1.$ If $\lambda(X)=m>0,$ then some open cover of $X$ has measure less than $m(1+\epsilon),$ so there has to be some interval in the open cover on which $X$ has $1/(1+\epsilon)$ of the interval's measure.

@FrançoisG.Dorais No, Lebesgue Density is a choiceless theorem. The standard proof doesn't use any choice.

@FrançoisG.Dorais A non-principal ultrafilter is a nonmeasurable set because it violates Lebesgue density. I think Raisonnier's Theorem is that an $\omega_1$-sequence of reals implies there is a nonmeasurable set, which I didn't use.

@EmilJeřábek Whether you have the test sets be bounded intervals or arbitrary $Y \subset \mathbb{R},$ you get equivalent definitions.

@NoahSchweber I'm not sure what large cardinals have to do with this. GCH is $\Pi^2_1$-conservative over ZF+DC. Unless you're referring to GCH being projectively conservative over ZF + large cardinals?

Re: "How large are the large cardinals one can justify using the idea of 'allowing to collect together everything we already had'?" This seems related to the often discussed matter in set theory of which large cardinals are justified by strong reflection principles. A good reference on this is Peter Koellner's "On Reflection Principles."

What could cause a problem is if HTT ever quantifies over arbitrary subsets of $V_{\kappa},$ e.g. if it quantifies over what $V_{\kappa}$ considers to be large categories. Note that $\kappa$ is inaccessible iff $V_{\kappa+1}$ satisfies the finitely axiomatizable theory NBG, so once you move up to the next layer of sets, there are sentences which distinguish inaccessible cardinals from those guaranteed by reflection.

It's also worth mentioning that, while some amount of choice is needed to prove that every ill-founded ordering has a descending sequence, this argument requires no choice since $A + B$ has an induced well-ordering from $A$ and $B,$ so this descending sequence can be canonically constructed.

That being said, the inductive argument you mention in the end seems fine, so I think the theorem still holds.

The proof of your last theorem doesn't seem right. Even $\text{ZFC}^-$ doesn't prove the reflection principle you described.