awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
have have : ∀ (this : IsGalois ℚ K),
  Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
Tactic: classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
have have₁ have₂ :
  ∀ (this : IsGalois ℚ K),
    Eq (α := Subgroup (ZMod n)ˣ)
      (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
            (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
          (stabilizer Gal(K/ℚ) P) :
        Subgroup (ZMod n)ˣ)
      (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
have h : ∀ (this : IsGalois ℚ K),
  (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            (stabilizer Gal(K/ℚ) P) :
          Subgroup (ZMod n)ˣ) :
      Set (ZMod n)ˣ) =
    (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
Tactic: classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
have have₁ have₂ :
  ∀ (this : IsGalois ℚ K),
    Eq (α := Subgroup (ZMod n)ˣ)
      (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
            (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
          (stabilizer Gal(K/ℚ) P) :
        Subgroup (ZMod n)ˣ)
      (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
h :
  ∀ (this : IsGalois ℚ K),
    (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
              (stabilizer Gal(K/ℚ) P) :
            Subgroup (ZMod n)ˣ) :
        Set (ZMod n)ˣ) =
      (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
have h₁ : ∀ (this : IsGalois ℚ K),
  (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
              (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
            (stabilizer Gal(K/ℚ) P) :
          Subgroup (ZMod n)ˣ) :
      Set (ZMod n)ˣ) ⊆
    (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
Tactic: classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst_3 : P.IsMaximal
inst_4 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
hn : p.Coprime n
have have₁ have₂ :
  ∀ (this : IsGalois ℚ K),
    Eq (α := Subgroup (ZMod n)ˣ)
      (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
            (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
          (stabilizer Gal(K/ℚ) P) :
        Subgroup (ZMod n)ˣ)
      (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
h :
  ∀ (this : IsGalois ℚ K),
    (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
              (stabilizer Gal(K/ℚ) P) :
            Subgroup (ZMod n)ˣ) :
        Set (ZMod n)ˣ) =
      (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
h₁ :
  ∀ (this : IsGalois ℚ K),
    (↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
              (stabilizer Gal(K/ℚ) P) :
            Subgroup (ZMod n)ˣ) :
        Set (ZMod n)ˣ) ⊆
      (↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ)
⊢ Eq (α := Subgroup (ZMod n)ˣ)
    (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
          (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
        (stabilizer Gal(K/ℚ) P) :
      Subgroup (ZMod n)ˣ)
    (Subgroup.zpowers (ZMod.unitOfCoprime p hn) : Subgroup (ZMod n)ˣ)
have h₂ : ∀ (this : IsGalois ℚ K),
  Fintype.card (↑(↑(Subgroup.zpowers (ZMod.unitOfCoprime p hn)) : Set (ZMod n)ˣ) : Type) ≤
    Fintype.card
      (↑(↑(((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
                    (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
                  (stabilizer Gal(K/ℚ) P) :
                Subgroup (ZMod n)ˣ) :
            Set (ZMod n)ˣ) :
        Type)
Tactic: classical
  have : IsGalois ℚ K := IsCyclotomicExtension.isGalois {n} ℚ K
  apply SetLike.ext'
  refine Set.eq_of_subset_of_card_le ?_ ?_
  · rintro _ ⟨σ, hσ, rfl⟩
    exact mem_zpowers_galEquivZMod_of_mem_stabilizer n K p P hn hσ
  · replace hn : ¬ p ∣ n := (Nat.Prime.coprime_iff_not_dvd hp.out).mp hn
    rw [Fintype.card_eq_nat_card, Fintype.card_eq_nat_card, SetLike.coe_sort_coe, Nat.card_zpowers,
      MulEquiv.mapSubgroup_apply, Subgroup.coe_map]
    change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)
    rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)})
      (by simp [hp.out.ne_zero]), inertiaDegIn_eq_of_not_dvd p K hn,
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsMulCommutative.{u_1} Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card.{u_2}
      ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((subgroupGalEquivSubgroupChar n K R :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ)) (Subgroup (DirichletCharacter R n))ᵒᵈ) :
                (a : Subgroup Gal(K/ℚ)) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
              H) :
          Subgroup (DirichletCharacter R n)) =
    Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)
have rw : Nat.card
    (HasQuotient.Quotient (ZMod n)ˣ (B := Subgroup (ZMod n)ˣ)
      (((MulEquiv.mapSubgroup (galEquivZMod n K) : Subgroup Gal(K/ℚ) ≃o Subgroup (ZMod n)ˣ) :
            (a : Subgroup Gal(K/ℚ)) → Subgroup (ZMod n)ˣ)
          H :
        Subgroup (ZMod n)ˣ)) =
  Nat.card.{u_1} (Gal(K/ℚ) ⧸ H)
Tactic: rw [subgroupGalEquivSubgroupChar, OrderIso.trans_apply, card_subgroupOrderIsoSubgroupMulChar]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card.{u_2}
      ↥(((OrderIso.trans IsGalois.intermediateFieldEquivSubgroup
                  (OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                    (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))))) :
                OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
              (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
            F :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
have rw : Nat.card.{u_2}
    ↥(((OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n)))) :
              OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))) :
            (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup (DirichletCharacter R n))
          ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F) :
        Subgroup (DirichletCharacter R n)) =
  Module.finrank.{0, u_1} ℚ ↥F
Tactic: rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
rw :
  Nat.card.{u_2}
      ↥(((OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                  (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n)))) :
                OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))) :
              (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
⊢ Nat.card.{u_2}
      ↥(((OrderIso.trans IsGalois.intermediateFieldEquivSubgroup
                  (OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                    (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))))) :
                OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
              (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
            F :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
have rw₁ : Nat.card.{u_2}
    ↥((OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))) :
            (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → Subgroup (DirichletCharacter R n))
          (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
              (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
            ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F)) :
        Subgroup (DirichletCharacter R n)) =
  Module.finrank.{0, u_1} ℚ ↥F
Tactic: rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
rw :
  Nat.card.{u_2}
      ↥(((OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                  (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n)))) :
                OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))) :
              (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → Subgroup (DirichletCharacter R n))
            ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
rw₁ :
  Nat.card.{u_2}
      ↥((OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))) :
              (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → Subgroup (DirichletCharacter R n))
            (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
                (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
              ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F)) :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
⊢ Nat.card.{u_2}
      ↥(((OrderIso.trans IsGalois.intermediateFieldEquivSubgroup
                  (OrderIso.trans (OrderIso.dual (subgroupGalEquivSubgroupChar n K R))
                    (OrderIso.symm (OrderIso.dualDual (Subgroup (DirichletCharacter R n))))) :
                OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
              (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
            F :
          Subgroup (DirichletCharacter R n)) =
    Module.finrank.{0, u_1} ℚ ↥F
have rw₂ : Nat.card.{u_2}
    ↥((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈ) → Subgroup (DirichletCharacter R n))
          ((OrderDual.ofDual : (a : (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈ)
            (((OrderIso.dual (subgroupGalEquivSubgroupChar n K R) :
                  OrderIso.{u_1, u_2} (Subgroup Gal(K/ℚ))ᵒᵈ (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ) :
                (a : (Subgroup Gal(K/ℚ))ᵒᵈ) → (Subgroup (DirichletCharacter R n))ᵒᵈᵒᵈ)
              ((IsGalois.intermediateFieldEquivSubgroup : (a : IntermediateField ℚ K) → (Subgroup Gal(K/ℚ))ᵒᵈ) F))) :
        Subgroup (DirichletCharacter R n)) =
  Module.finrank.{0, u_1} ℚ ↥F
Tactic: rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw : Membership.mem (γ := Subgroup (DirichletCharacter R n))
    (((intermediateFieldEquivSubgroupChar n K R :
            OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
          (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
        F :
      Subgroup (DirichletCharacter R n))
    χ ↔
  m ∈ χ.conductorSet
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst_3 : CommRing R
inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_5 : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst_6 : NeZero m
inst_7 : IsGalois.{0, u_1} ℚ ↥F
inst_8 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
simp_rw :
  Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    m ∈ χ.conductorSet
⊢ Membership.mem (γ := Subgroup (DirichletCharacter R n))
      (((intermediateFieldEquivSubgroupChar n K R :
              OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
            (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
          F :
        Subgroup (DirichletCharacter R n))
      χ ↔
    χ.conductor ∣ m
have simp_rw₁ : Membership.mem (γ := Subgroup (DirichletCharacter R n))
    (((intermediateFieldEquivSubgroupChar n K R :
            OrderIso.{u_1, u_2} (IntermediateField ℚ K) (Subgroup (DirichletCharacter R n))) :
          (a : IntermediateField ℚ K) → Subgroup (DirichletCharacter R n))
        F :
      Subgroup (DirichletCharacter R n))
    χ ↔
  χ.FactorsThrough m
Tactic: simp_rw [← χ.mem_conductorSet_iff_conductor_dvd hdiv, χ.mem_conductorSet_iff,
    factorsThrough_iff_ker_unitsMap hdiv, mem_intermediateFieldEquivSubgroupChar_iff,
    SetLike.le_def, ← (galEquivZMod n K).forall_congr_right, MonoidHom.mem_ker,
    MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe, ← (galEquivZMod_restrictNormal_apply n K F hdiv _),
    EmbeddingLike.map_eq_one_iff, AlgEquiv.restrictNormal_eq_one_iff,
    IntermediateField.mem_fixingSubgroup_iff, Units.ext_iff, toUnitHom_eq, coe_equivToUnitHom,
    Units.val_one]