Porting note: was tidy

[pitmonticone]

Classifies porting notes claiming anything semantically equivalent to:

• "used to be tidy"
• "was tidy "

Examples

mathlib4/Archive/Imo/Imo1998Q2.lean

Lines 149 to 156 in 6af752e

	theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
	(agreedContestants r p).card =
	((A r).filter fun a : AgreedTriple C J => a.judgePair = p).card := by
	rw [A_fibre_over_judgePair r h]
	apply Finset.card_image_of_injOn
	-- porting note: used to be `tidy`
	unfold Set.InjOn; intros; ext; all_goals aesop
	#align imo1998_q2.A_fibre_over_judge_pair_card Imo1998Q2.A_fibre_over_judgePair_card

mathlib4/Mathlib/CategoryTheory/Limits/KanExtension.lean

Lines 160 to 172 in 6af752e

	/-- The right Kan extension of a functor. -/
	@[simps!]
	def ran [∀ X, HasLimitsOfShape (StructuredArrow X ι) D] : (S ⥤ D) ⥤ L ⥤ D :=
	Adjunction.rightAdjointOfEquiv (fun F G => (Ran.equiv ι G F).symm) (by {
	-- Porting note: was `tidy`
	intros X' X Y f g
	ext t
	apply limit.hom_ext
	intros j
	dsimp [Ran.equiv]
	simp })
	set_option linter.uppercaseLean3 false in
	#align category_theory.Ran CategoryTheory.ran