feat(model_theory/substructures): tweak universes for `lift_card_clos…

…ure_le` (#14597) Since `cardinal.lift.{(max u v) u} = cardinal.lift.{v u}`, the latter form should be preferred.
leanprover-community · Jun 8, 2022 · d315666 · d315666
1 parent 8934884
commit d315666
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/model_theory/substructures.lean b/src/model_theory/substructures.lean
@@ -262,11 +262,12 @@ begin
   exact cardinal.mk_range_le_lift,
 end
 
-theorem lift_card_closure_le : cardinal.lift.{(max u w) w} (# (closure L s)) ≤
-  max ℵ₀ (cardinal.lift.{(max u w) w} (#s) + cardinal.lift.{(max u w) u} (#(Σ i, L.functions i))) :=
+theorem lift_card_closure_le : cardinal.lift.{u w} (# (closure L s)) ≤
+  max ℵ₀ (cardinal.lift.{u w} (#s) + cardinal.lift.{w u} (#(Σ i, L.functions i))) :=
 begin
+  rw ←lift_umax,
   refine lift_card_closure_le_card_term.trans (term.card_le.trans _),
-  rw [mk_sum, lift_umax', lift_umax],
+  rw [mk_sum, lift_umax],
 end
 
 variable (L)