-- Mathlib/SetTheory/Cardinal/UnivLE.lean
theorem univLE_iff_cardinal_le : UnivLE.{u, v} ↔ univ.{u, v+1} ≤ univ.{v, u+1}

Proof state:
case refine_2.intro.mk
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
use α

Result:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Proof state:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
exact le.trans_lt (lift_lt_univ'.{u,v+1} #α)

Result:
no goals

Proof state:
⊢ UnivLE.{u, v} ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
rw [← not_iff_not, UnivLE]

Result:
⊢ (¬∀ (α : Type u), Small.{v, u} α) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}

Proof state:
case refine_2
h : univ.{v, u + 1} < univ.{u, v + 1}
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
obtain ⟨⟨α⟩, h⟩ := lt_univ'.mp h

Result:
case refine_2.intro.mk
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Proof state:
⊢ (∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

case refine_2
h : univ.{v, u + 1} < univ.{u, v + 1}
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Proof state:
⊢ (¬∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
push_neg

Result:
⊢ (∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}

Proof state:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α

Tactic:
exact h.le

Result:
no goals

Proof state:
⊢ (¬∀ (α : Type u), Small.{v, u} α) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
simp_rw [small_iff_lift_mk_lt_univ]

Result:
⊢ (¬∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}

Proof state:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
rw [univ_umax.{v,u}, ← lift_le.{u+1}, lift_univ, lift_lift] at le

Result:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

Proof state:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
rw [univ_umax.{v,u}, ← lift_le.{u+1}, lift_univ, lift_lift]

Result:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α