awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x_1)
⊢ x = x_1
have refine_1 : ∀
  (h :
    Eq (α := OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ)
      { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x, map_one' := sorry }
      { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1, map_one' := sorry }),
  x = x_1
Tactic: rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x_1)
refine_1 :
  ∀
    (h :
      Eq (α := OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ)
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x, map_one' := ⋯ }
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1, map_one' := ⋯ }),
    x = x_1
⊢ x = x_1
have refine_1₁ : ∀
  (h :
    Eq (α := MonoidHom.{u_1, u_2} G Mˣ → Mˣ) (fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x)
      fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1),
  x = x_1
Tactic: rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x_1)
refine_1 :
  ∀
    (h :
      Eq (α := OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ)
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x, map_one' := ⋯ }
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1, map_one' := ⋯ }),
    x = x_1
refine_1₁ :
  ∀
    (h :
      Eq (α := MonoidHom.{u_1, u_2} G Mˣ → Mˣ) (fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x)
        fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1),
    x = x_1
⊢ x = x_1
have refine_1₂ : ∀
  (h :
    ∀ (x_2 : MonoidHom.{u_1, u_2} G Mˣ),
      Eq.{u_2 + 1} (α := Mˣ) ((x_2 : (a : G) → Mˣ) x : Mˣ) ((x_2 : (a : G) → Mˣ) x_1 : Mˣ)),
  x = x_1
Tactic: rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
h :
  Eq (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x)
    ((fun (g : G) ↦
        ({ toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ))
      x_1)
refine_1 :
  ∀
    (h :
      Eq (α := OneHom (MonoidHom.{u_1, u_2} G Mˣ) Mˣ)
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x, map_one' := ⋯ }
        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1, map_one' := ⋯ }),
    x = x_1
refine_1₁ :
  ∀
    (h :
      Eq (α := MonoidHom.{u_1, u_2} G Mˣ → Mˣ) (fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x)
        fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) x_1),
    x = x_1
refine_1₂ :
  ∀
    (h :
      ∀ (x_2 : MonoidHom.{u_1, u_2} G Mˣ),
        Eq.{u_2 + 1} (α := Mˣ) ((x_2 : (a : G) → Mˣ) x : Mˣ) ((x_2 : (a : G) → Mˣ) x_1 : Mˣ)),
    x = x_1
⊢ x = x_1
have refine_1₃ : ∀ (h : x = x_1), x = x_1
Tactic: rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
⊢ Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
have refine_2 : Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ)
Tactic: rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
refine_2 : Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ)
⊢ Nat.card G = Nat.card (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
have refine_2₁ : Nat.card G = Nat.card G
Tactic: rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
x x_1 : G
⊢ (Equiv.ofBijective
          (fun (g : G) ↦
            { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
          ⋯ :
        (a : G) → (G →* Mˣ) →* Mˣ)
      (x * x_1) =
    HMul.hMul (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
      ((Equiv.ofBijective
              (fun (g : G) ↦
                { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
              ⋯ :
            (a : G) → (G →* Mˣ) →* Mˣ)
          x :
        MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
      ((Equiv.ofBijective
              (fun (g : G) ↦
                { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := ⋯, map_mul' := ⋯ :
                  MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
              ⋯ :
            (a : G) → (G →* Mˣ) →* Mˣ)
          x_1 :
        MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
have h : ∀ (x_2 : MonoidHom.{u_1, u_2} G Mˣ),
  Eq.{u_2 + 1} (α := M)
    (↑((((Equiv.ofBijective
                    (fun (g : G) ↦
                      { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := sorry,
                        map_mul' := sorry : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                    sorry :
                  (a : G) → (G →* Mˣ) →* Mˣ)
                (x * x_1) :
              MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
            (a : G →* Mˣ) → Mˣ)
          x_2) :
      M)
    (↑((HMul.hMul (α := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) (β := MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
              ((Equiv.ofBijective
                      (fun (g : G) ↦
                        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := sorry,
                          map_mul' := sorry : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                      sorry :
                    (a : G) → (G →* Mˣ) →* Mˣ)
                  x :
                MonoidHom.{u_1, u_2} G Mˣ →* Mˣ)
              ((Equiv.ofBijective
                      (fun (g : G) ↦
                        { toFun := fun (φ : MonoidHom.{u_1, u_2} G Mˣ) ↦ (φ : (a : G) → Mˣ) g, map_one' := sorry,
                          map_mul' := sorry : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ })
                      sorry :
                    (a : G) → (G →* Mˣ) →* Mˣ)
                  x_1 :
                MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
            (a : G →* Mˣ) → Mˣ)
          x_2) :
      M)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
φ : MonoidHom.{u_1, u_2} G Mˣ
η : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ
⊢ Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) : Mˣ)
    ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
have rw : Eq.{u_2 + 1} (α := Mˣ)
  ((((MulEquiv.symm (monoidHomMonoidHomEquiv G M) : (a : G) → (G →* Mˣ) →* Mˣ)
            ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) :
          MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
        (a : G →* Mˣ) → Mˣ)
      φ :
    Mˣ)
  ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
Tactic: rw [← monoidHomMonoidHomEquiv_symm_apply_apply G M (monoidHomMonoidHomEquiv G M η) φ,
    MulEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
φ : MonoidHom.{u_1, u_2} G Mˣ
η : MonoidHom.{u_1, u_2} G Mˣ →* Mˣ
rw :
  Eq.{u_2 + 1} (α := Mˣ)
    ((((MulEquiv.symm (monoidHomMonoidHomEquiv G M) : (a : G) → (G →* Mˣ) →* Mˣ)
              ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) :
            MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) :
          (a : G →* Mˣ) → Mˣ)
        φ :
      Mˣ)
    ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
⊢ Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) ((monoidHomMonoidHomEquiv G M : (a : (G →* Mˣ) →* Mˣ) → G) η) : Mˣ)
    ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
have rw₁ : Eq.{u_2 + 1} (α := Mˣ) ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ) ((η : (a : G →* Mˣ) → Mˣ) φ : Mˣ)
Tactic: rw [← monoidHomMonoidHomEquiv_symm_apply_apply G M (monoidHomMonoidHomEquiv G M η) φ,
    MulEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
⊢ (fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
        ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
            (ker (M :=
              ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                    Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                Mˣ)
              (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                  ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                        Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                    Mˣ)) :
          Subgroup G))
      ((fun (H : Subgroup G) ↦
          ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
              (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
            (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
        H) =
    H
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G)
      ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
          ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
              (ker (M :=
                ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                      Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                  Mˣ)
                (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                  (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)) :
            Subgroup G))
        ((fun (H : Subgroup G) ↦
            ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
              (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
          H))
      x ↔
    x ∈ H
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (hypothesis)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
⊢ (fun (H : Subgroup G) ↦
        ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
            (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
          (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
      ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
          ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
              (ker (M :=
                ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                      Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                  Mˣ)
                (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                  (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)) :
            Subgroup G))
        Φ) =
    Φ
have this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
Tactic: have : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ)) := by
      rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
⊢ (fun (H : Subgroup G) ↦
        ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
            (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
          (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
      ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
          ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
              (ker (M :=
                ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                      Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                  Mˣ)
                (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                  (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)) :
            Subgroup G))
        Φ) =
    Φ
have h : ∀ (φ : MonoidHom.{u_1, u_2} G Mˣ),
  Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
        ((fun (H : Subgroup G) ↦
            ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
              (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
          ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
              ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)) :
                Subgroup G))
            Φ)))
      φ ↔
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (MonoidHom.{u_1, u_2} G Mˣ))
φ : MonoidHom.{u_1, u_2} G Mˣ
⊢ Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ))
        ((fun (H : Subgroup G) ↦
            ((OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)) :
              (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ))
          ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
              ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)) :
                Subgroup G))
            Φ)))
      φ ↔
    Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
      φ
have h : (∀ (x : G),
    Membership.mem (γ := Subgroup G)
        ((fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
            ((MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                (ker (M :=
                  ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                        Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                    Mˣ)
                  (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                    (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                      ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                            Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                        Mˣ)) :
              Subgroup G))
          Φ)
        x →
      Eq.{u_2 + 1} (α := Mˣ) ((φ : (a : G) → Mˣ) x : Mˣ) (1 : Mˣ)) ↔
  Membership.mem (γ := Subgroup (MonoidHom.{u_1, u_2} G Mˣ))
    ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ : Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) φ
Tactic: rw [OrderDual.ofDual_toDual, mem_ker, restrictHom_apply, restrict_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Duality (goal)
Goal:
G : Type u_1
M : Type u_2
inst : CommGroup G
inst_1 : Finite G
inst_2 : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
⊢ LE.le (α := (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ)
      (({
              toFun := fun (H : Subgroup G) ↦
                (OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                  (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)),
              invFun := fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
                (MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ)
          H₁ :
        (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ)
      (({
              toFun := fun (H : Subgroup G) ↦
                (OrderDual.toDual : (a : Subgroup (G →* Mˣ)) → (Subgroup (G →* Mˣ))ᵒᵈ)
                  (ker (M := MonoidHom.{u_1, u_2} (↥H) Mˣ) (restrictHom H Mˣ)),
              invFun := fun (Φ : (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↦
                (MulEquiv.mapSubgroup (monoidHomMonoidHomEquiv G M) : (a : Subgroup ((G →* Mˣ) →* Mˣ)) → Subgroup G)
                  (ker (M :=
                    ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                          Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                      Mˣ)
                    (restrictHom ((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ) Mˣ :
                      (MonoidHom.{u_1, u_2} G Mˣ →* Mˣ) →*
                        ↥((OrderDual.ofDual : (a : (Subgroup (G →* Mˣ))ᵒᵈ) → Subgroup (G →* Mˣ)) Φ :
                              Subgroup (MonoidHom.{u_1, u_2} G Mˣ)) →*
                          Mˣ)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subgroup G) → (Subgroup (G →* Mˣ))ᵒᵈ)
          H₂ :
        (Subgroup (MonoidHom.{u_1, u_2} G Mˣ))ᵒᵈ) ↔
    H₁ ≤ H₂
have simp_rw : (∀ ⦃x : MonoidHom.{u_1, u_2} G Mˣ⦄,
    (∀ x_1 ∈ H₂, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) →
      ∀ x_1 ∈ H₁, Eq.{u_2 + 1} (α := Mˣ) ((x : (a : G) → Mˣ) x_1 : Mˣ) (1 : Mˣ)) ↔
  ∀ ⦃x : G⦄, x ∈ H₁ → x ∈ H₂
Tactic: simp_rw [Equiv.coe_fn_mk, OrderDual.toDual_le_toDual,
      SetLike.le_def, mem_ker, restrictHom_apply, restrict_eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteIndexNormalSubgroup (goal)
Goal:
G : Type u_1
inst : Group G
A B : FiniteIndexNormalSubgroup G
h :
  Eq.{u_1 + 1} (α := Subgroup G) ((fun (H : FiniteIndexNormalSubgroup G) ↦ H.toSubgroup) A)
    ((fun (H : FiniteIndexNormalSubgroup G) ↦ H.toSubgroup) B)
⊢ A = B
have carrier : ∀ (x : G), x ∈ A.carrier ↔ x ∈ B.carrier
Tactic: ext