Skip to content

Commit 9aa0dc7

Browse files
[pre-commit.ci lite] apply automatic fixes
1 parent 8971777 commit 9aa0dc7

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/SetTheory/Cardinal/Cofinality

Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ theorem ord_cof_eq_isClub_of_isCofinal (hs : IsCofinal s) (hsα : typeLT s = (co
178178
refine fun x hx ↦ ⟨.mk ⟨f.symm ⟨x, hx⟩ + 1, ?_⟩, ?_⟩
179179
· exact (isSuccLimit_ord hα.le).add_one_lt (ToType.toOrd_lt _)
180180
· unfold g
181-
convert limitRecOn_add_one ..
181+
convert limitRecOn_add_one ..
182182
refine ⟨range g, hsg, ⟨?_, hs.mono hsg⟩, ?_⟩
183183
· sorry
184184
· conv_rhs => rw [← hsα]

0 commit comments

Comments
 (0)