feat(data/sigma,data/ulift,logic/equiv): add missing lemmas (#14903)

Add lemmas and `equiv`s about `plift`, `psigma`, and `pprod`.

src/data/sigma/basic.lean

@@ -192,6 +192,14 @@ by { cases x₀, cases x₁, cases h₀, cases h₁, refl }
 lemma ext_iff {x₀ x₁ : psigma β} : x₀ = x₁ ↔ x₀.1 = x₁.1 ∧ x₀.2 == x₁.2 :=
 by { cases x₀, cases x₁, exact psigma.mk.inj_iff }
 
+@[simp] theorem «forall» {p : (Σ' a, β a) → Prop} :
+  (∀ x, p x) ↔ (∀ a b, p ⟨a, b⟩) :=
+⟨assume h a b, h ⟨a, b⟩, assume h ⟨a, b⟩, h a b⟩
+
+@[simp] theorem «exists» {p : (Σ' a, β a) → Prop} :
+  (∃ x, p x) ↔ (∃ a b, p ⟨a, b⟩) :=
+⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
+
 /-- A specialized ext lemma for equality of psigma types over an indexed subtype. -/
 @[ext]
 lemma subtype_ext {β : Sort*} {p : α → β → Prop} :

src/data/ulift.lean

@@ -14,6 +14,7 @@ In this file we provide `subsingleton`, `unique`, `decidable_eq`, and `is_empty`
 -/
 
 universes u v
+open function
 
 namespace plift
 
@@ -24,11 +25,20 @@ instance [unique α] : unique (plift α) := equiv.plift.unique
 instance [decidable_eq α] : decidable_eq (plift α) := equiv.plift.decidable_eq
 instance [is_empty α] : is_empty (plift α) := equiv.plift.is_empty
 
+lemma up_injective : injective (@up α) := equiv.plift.symm.injective
+lemma up_surjective : surjective (@up α) := equiv.plift.symm.surjective
+lemma up_bijective : bijective (@up α) := equiv.plift.symm.bijective
+
+@[simp] lemma up_inj {x y : α} : up x = up y ↔ x = y := up_injective.eq_iff
+
+lemma down_surjective : surjective (@down α) := equiv.plift.surjective
+lemma down_bijective : bijective (@down α) := equiv.plift.bijective
+
 @[simp] lemma «forall» {p : plift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (plift.up x) :=
-equiv.plift.forall_congr_left'
+up_surjective.forall
 
 @[simp] lemma «exists» {p : plift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (plift.up x) :=
-equiv.plift.exists_congr_left
+up_surjective.exists
 
 end plift
 
@@ -41,10 +51,19 @@ instance [unique α] : unique (ulift α) := equiv.ulift.unique
 instance [decidable_eq α] : decidable_eq (ulift α) := equiv.ulift.decidable_eq
 instance [is_empty α] : is_empty (ulift α) := equiv.ulift.is_empty
 
+lemma up_injective : injective (@up α) := equiv.ulift.symm.injective
+lemma up_surjective : surjective (@up α) := equiv.ulift.symm.surjective
+lemma up_bijective : bijective (@up α) := equiv.ulift.symm.bijective
+
+@[simp] lemma up_inj {x y : α} : up x = up y ↔ x = y := up_injective.eq_iff
+
+lemma down_surjective : surjective (@down α) := equiv.ulift.surjective
+lemma down_bijective : bijective (@down α) := equiv.ulift.bijective
+
 @[simp] lemma «forall» {p : ulift α → Prop} : (∀ x, p x) ↔ ∀ x : α, p (ulift.up x) :=
-equiv.ulift.forall_congr_left'
+up_surjective.forall
 
 @[simp] lemma «exists» {p : ulift α → Prop} : (∃ x, p x) ↔ ∃ x : α, p (ulift.up x) :=
-equiv.ulift.exists_congr_left
+up_surjective.exists
 
 end ulift

src/logic/equiv/basic.lean

@@ -394,6 +394,14 @@ def pprod_equiv_prod {α β : Type*} : pprod α β ≃ α × β :=
   left_inv := λ ⟨x, y⟩, rfl,
   right_inv := λ ⟨x, y⟩, rfl }
 
+/-- `pprod α β` is equivalent to `plift α × plift β` -/
+@[simps apply symm_apply]
+def pprod_equiv_prod_plift {α β : Sort*} : pprod α β ≃ plift α × plift β :=
+{ to_fun := λ x, (plift.up x.1, plift.up x.2),
+  inv_fun := λ x, ⟨x.1.down, x.2.down⟩,
+  left_inv := λ ⟨x, y⟩, rfl,
+  right_inv := λ ⟨⟨x⟩, ⟨y⟩⟩, rfl }
+
 /-- equivalence of propositions is the same as iff -/
 def of_iff {P Q : Prop} (h : P ↔ Q) : P ≃ Q :=
 { to_fun := h.mp,
@@ -941,10 +949,16 @@ def Pi_curry {α} {β : α → Sort*} (γ : Π a, β a → Sort*) :
 end
 
 section
+
 /-- A `psigma`-type is equivalent to the corresponding `sigma`-type. -/
 @[simps apply symm_apply] def psigma_equiv_sigma {α} (β : α → Type*) : (Σ' i, β i) ≃ Σ i, β i :=
 ⟨λ a, ⟨a.1, a.2⟩, λ a, ⟨a.1, a.2⟩, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
 
+/-- A `psigma`-type is equivalent to the corresponding `sigma`-type. -/
+@[simps apply symm_apply] def psigma_equiv_sigma_plift {α} (β : α → Sort*) :
+  (Σ' i, β i) ≃ Σ i : plift α, plift (β i.down) :=
+⟨λ a, ⟨plift.up a.1, plift.up a.2⟩, λ a, ⟨a.1.down, a.2.down⟩, λ ⟨a, b⟩, rfl, λ ⟨⟨a⟩, ⟨b⟩⟩, rfl⟩
+
 /-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ' a, β₁ a` and
 `Σ' a, β₂ a`. -/
 @[simps apply]

src/set_theory/cardinal/cofinality.lean

@@ -218,13 +218,15 @@ begin
 end
 
 @[simp] theorem lift_cof (o) : (cof o).lift = cof o.lift :=
-induction_on o $ begin introsI α r _,
+begin
+  refine induction_on o _,
+  introsI α r _,
   cases lift_type r with _ e, rw e,
   apply le_antisymm,
   { unfreezingI { refine le_cof_type.2 (λ S H, _) },
-    have : (#(ulift.up ⁻¹' S)).lift ≤ #S :=
-     ⟨⟨λ ⟨⟨x, h⟩⟩, ⟨⟨x⟩, h⟩,
-       λ ⟨⟨x, h₁⟩⟩ ⟨⟨y, h₂⟩⟩ e, by simp at e; congr; injection e⟩⟩,
+    have : (#(ulift.up ⁻¹' S)).lift ≤ #S,
+    { rw [← cardinal.lift_umax, ← cardinal.lift_id' (#S)],
+      exact mk_preimage_of_injective_lift ulift.up _ ulift.up_injective },
     refine (cardinal.lift_le.2 $ cof_type_le _).trans this,
     exact λ a, let ⟨⟨b⟩, bs, br⟩ := H ⟨a⟩ in ⟨b, bs, br⟩ },
   { rcases cof_eq r with ⟨S, H, e'⟩,