chore(data/fintype/basic): fintype α/β from fintype α ⊕ β (#7736)

Also renaming the equivalent `α × β` versions, for consistency.



Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

src/data/fintype/basic.lean

@@ -733,12 +733,12 @@ rfl
 card_product _ _
 
 /-- Given that `α × β` is a fintype, `α` is also a fintype. -/
-def fintype.fintype_prod_left {α β} [decidable_eq α] [fintype (α × β)] [nonempty β] : fintype α :=
+def fintype.prod_left {α β} [decidable_eq α] [fintype (α × β)] [nonempty β] : fintype α :=
 ⟨(fintype.elems (α × β)).image prod.fst,
   assume a, let ⟨b⟩ := ‹nonempty β› in by simp; exact ⟨b, fintype.complete _⟩⟩
 
 /-- Given that `α × β` is a fintype, `β` is also a fintype. -/
-def fintype.fintype_prod_right {α β} [decidable_eq β] [fintype (α × β)] [nonempty α] : fintype β :=
+def fintype.prod_right {α β} [decidable_eq β] [fintype (α × β)] [nonempty α] : fintype β :=
 ⟨(fintype.elems (α × β)).image prod.snd,
   assume b, let ⟨a⟩ := ‹nonempty α› in by simp; exact ⟨a, fintype.complete _⟩⟩
 
@@ -763,6 +763,16 @@ instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕
   ((equiv.sum_equiv_sigma_bool _ _).symm.trans
     (equiv.sum_congr equiv.ulift equiv.ulift))
 
+/-- Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses
+that `sum.inl` is an injection, but there's no clear inverse if `α` is empty. -/
+noncomputable def fintype.sum_left {α β} [fintype (α ⊕ β)] : fintype α :=
+fintype.of_injective (sum.inl : α → α ⊕ β) sum.inl_injective
+
+/-- Given that `α ⊕ β` is a fintype, `β` is also a fintype. This is non-computable as it uses
+that `sum.inr` is an injection, but there's no clear inverse if `β` is empty. -/
+noncomputable def fintype.sum_right {α β} [fintype (α ⊕ β)] : fintype β :=
+fintype.of_injective (sum.inr : β → α ⊕ β) sum.inr_injective
+
 namespace fintype
 variables [fintype α] [fintype β]
 

src/group_theory/order_of_element.lean

@@ -736,9 +736,9 @@ begin
   have ft_prod : fintype (quotient (gpowers x) × (gpowers x)),
     from fintype.of_equiv G group_equiv_quotient_times_subgroup,
   have ft_s : fintype (gpowers x),
-    from @fintype.fintype_prod_right _ _ _ ft_prod _,
+    from @fintype.prod_right _ _ _ ft_prod _,
   have ft_cosets : fintype (quotient (gpowers x)),
-    from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, (gpowers x).one_mem⟩⟩,
+    from @fintype.prod_left _ _ _ ft_prod ⟨⟨1, (gpowers x).one_mem⟩⟩,
   have eq₁ : fintype.card G = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
     from calc fintype.card G = @fintype.card _ ft_prod :
         @fintype.card_congr _ _ _ ft_prod group_equiv_quotient_times_subgroup