-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite M
inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent.{u_1} Mˣ)
H : Subgroup Mˣ
rw :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((OrderIso.trans (CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R)
                  (OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom))) :
                (a : Subgroup Mˣ) → (Subgroup (MulChar M R))ᵒᵈ)
              H) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₁ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            (((OrderIso.dual (MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom)) :
                  (Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ))ᵒᵈ ≃o (Subgroup (MulChar M R))ᵒᵈ) :
                (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → (Subgroup (MulChar M R))ᵒᵈ)
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₂ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((OrderDual.toDual : (a : Subgroup (MulChar M R)) → (Subgroup (MulChar M R))ᵒᵈ)
              ((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) :
                  (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
                ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
                  ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ)
                    H)))) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₃ :
  Nat.card
      ↥((MulEquiv.mapSubgroup (MulEquiv.symm mulEquivToUnitHom) : (a : Subgroup (Mˣ →* Rˣ)) → Subgroup (MulChar M R))
            ((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
              ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H)) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₄ :
  Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (Mˣ →* Rˣ))ᵒᵈ) → Subgroup (Mˣ →* Rˣ))
            ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R : (a : Subgroup Mˣ) → (Subgroup (Mˣ →* Rˣ))ᵒᵈ) H) :
          Subgroup (MonoidHom.{u_1, u_2} Mˣ Rˣ)) =
    Nat.card.{u_1} (Mˣ ⧸ H)
rw₅ rw₆ : Nat.card.{u_1} (Mˣ ⧸ H) = Nat.card.{u_1} (Mˣ ⧸ H)
⊢ Nat.card
      ↥((OrderDual.ofDual : (a : (Subgroup (MulChar M R))ᵒᵈ) → Subgroup (MulChar M R))
            ((subgroupOrderIsoSubgroupMulChar M R : (a : Subgroup Mˣ) → (Subgroup (MulChar M R))ᵒᵈ) H) :
          Subgroup (MulChar M R)) =
    Nat.card.{u_1} (Mˣ ⧸ H)

Tactic:
rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
    OrderDual.ofDual_toDual, Subgroup.card_mapSubgroup,
    CommGroup.card_subgroupOrderIsoSubgroupMonoidHom]

Premises used: OrderIso.dual_apply, OrderIso.trans_apply, Subgroup.card_mapSubgroup, CommGroup.card_subgroupOrderIsoSubgroupMonoidHom, MulChar.subgroupOrderIsoSubgroupMulChar, OrderDual.ofDual_toDual