-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_card : orderOf x ∣ Fintype.card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
⊢ orderOf x ∣ card G

Tactic:
have eq₁ : Fintype.card G = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
  calc
    Fintype.card G = @Fintype.card _ ft_prod :=
      @Fintype.card_congr _ _ _ ft_prod groupEquivQuotientProdSubgroup
    _ = @Fintype.card _ (@instFintypeProd _ _ ft_cosets ft_s) :=
      congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
    _ = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
      @Fintype.card_prod _ _ ft_cosets ft_s

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
⊢ orderOf x ∣ card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
classical
  have ft_prod : Fintype ((G ⧸ zpowers x) × zpowers x) :=
    Fintype.ofEquiv G groupEquivQuotientProdSubgroup
  have ft_s : Fintype (zpowers x) := @Fintype.prodRight _ _ _ ft_prod _
  have ft_cosets : Fintype (G ⧸ zpowers x) :=
    @Fintype.prodLeft _ _ _ ft_prod ⟨⟨1, (zpowers x).one_mem⟩⟩
  have eq₁ : Fintype.card G = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
    calc
      Fintype.card G = @Fintype.card _ ft_prod :=
        @Fintype.card_congr _ _ _ ft_prod groupEquivQuotientProdSubgroup
      _ = @Fintype.card _ (@instFintypeProd _ _ ft_cosets ft_s) :=
        congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
      _ = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
        @Fintype.card_prod _ _ ft_cosets ft_s
  have eq₂ : orderOf x = @Fintype.card _ ft_s :=
    calc
      orderOf x = _ := Fintype.card_zpowers.symm
      _ = _ := congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
  exact Dvd.intro (@Fintype.card (G ⧸ Subgroup.zpowers x) ft_cosets) (by rw [eq₁, eq₂, mul_comm])

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
⊢ orderOf x ∣ card G

Tactic:
have ft_s : Fintype (zpowers x) := @Fintype.prodRight _ _ _ ft_prod _

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
⊢ orderOf x ∣ card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
have ft_prod : Fintype ((G ⧸ zpowers x) × zpowers x) :=
  Fintype.ofEquiv G groupEquivQuotientProdSubgroup

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
⊢ orderOf x ∣ card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
⊢ orderOf x ∣ card G

Tactic:
have eq₂ : orderOf x = @Fintype.card _ ft_s :=
  calc
    orderOf x = _ := Fintype.card_zpowers.symm
    _ = _ := congr_arg (@Fintype.card _) <| Subsingleton.elim _ _

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
eq₂ : orderOf x = card ↥(zpowers x)
⊢ orderOf x ∣ card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
⊢ orderOf x ∣ card G

Tactic:
have ft_cosets : Fintype (G ⧸ zpowers x) :=
  @Fintype.prodLeft _ _ _ ft_prod ⟨⟨1, (zpowers x).one_mem⟩⟩

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
⊢ orderOf x ∣ card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
eq₂ : orderOf x = card ↥(zpowers x)
⊢ orderOf x ∣ card G

Tactic:
exact Dvd.intro (@Fintype.card (G ⧸ Subgroup.zpowers x) ft_cosets) (by rw [eq₁, eq₂, mul_comm])

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
ft_prod : Fintype ((G ⧸ zpowers x) × ↥(zpowers x))
ft_s : Fintype ↥(zpowers x)
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : card G = card (G ⧸ zpowers x) * card ↥(zpowers x)
eq₂ : orderOf x = card ↥(zpowers x)
⊢ orderOf x * card (G ⧸ zpowers x) = card G

Tactic:
rw [eq₁, eq₂, mul_comm]

Result:
no goals