awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Fintype.card G ≤ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)

Tactic:
Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)

Premises used: Fintype.card_le_of_injective, MulSemiringAction.toAlgHom_injective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Fintype.card G ≤ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)

Tactic:
exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)

Premises used: Fintype.card_le_of_injective, MulSemiringAction.toAlgHom_injective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
intro : Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F
⊢ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Tactic:
rw [← finrank_eq_card G F]

Premises used: FixedPoints.finrank_eq_card
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F

Tactic:
LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)

Premises used: LE.le.trans_eq, finrank_algHom, Module.finrank_linearMap_self
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
val : Fintype G
⊢ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F

Tactic:
exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)

Premises used: LE.le.trans_eq, finrank_algHom, Module.finrank_linearMap_self
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := Gal(F/↥(subfield G F)))
    (⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F) : (a : G) → Gal(F/↥(subfield G F)))

Tactic:
⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
    fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩

Premises used: AlgEquiv.toAlgHom, Exists.imp, Function.Bijective.injective, Function.Bijective.surjective, And.intro, FixedPoints.toAlgHom_bijective, Function.Bijective
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
refine_1 :
  ∀ (x x_1 : G)
    (h :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield G F)))
        (((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
              (a : G) → Gal(F/↥(subfield G F)))
            x :
          Gal(F/↥(subfield G F)))
        (((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
              (a : G) → Gal(F/↥(subfield G F)))
            x_1 :
          Gal(F/↥(subfield G F)))),
    Eq (α := F →ₐ[↥(subfield G F)] F) (MulSemiringAction.toAlgHom (↥(subfield G F)) F x)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F x_1)
refine_2 :
  ∀ (f : Gal(F/↥(subfield G F))) (x : G)
    (h : MulSemiringAction.toAlgHom (↥(subfield G F)) F x = (↑f : F →ₐ[↥(subfield G F)] F)),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        x =
      f
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := Gal(F/↥(subfield G F)))
    (⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F) : (a : G) → Gal(F/↥(subfield G F)))

Tactic:
refine ⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
    fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
x x_1 : G
h :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield G F)))
    (((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        x :
      Gal(F/↥(subfield G F)))
    (((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        x_1 :
      Gal(F/↥(subfield G F)))
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀
    (h :
      ∀ (x_2 : F),
        Eq (α := F)
          (((((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
                      (a : G) → Gal(F/↥(subfield G F)))
                    x :
                  Gal(F/↥(subfield G F))) :
                (a : F) → F)
              x_2 :
            F)
          (((((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
                      (a : G) → Gal(F/↥(subfield G F)))
                    x_1 :
                  Gal(F/↥(subfield G F))) :
                (a : F) → F)
              x_2 :
            F))
    (x_2 : F),
    Eq (α := F) ((MulSemiringAction.toAlgHom (↥(subfield G F)) F x : (a : F) → F) x_2 : F)
      ((MulSemiringAction.toAlgHom (↥(subfield G F)) F x_1 : (a : F) → F) x_2 : F)
⊢ Eq (α := F →ₐ[↥(subfield G F)] F) (MulSemiringAction.toAlgHom (↥(subfield G F)) F x)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F x_1)

Tactic:
rwa [DFunLike.ext_iff] at h ⊢

Premises used: DFunLike.ext_iff
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
inst_4 : FaithfulSMul G F
f : Gal(F/↥(subfield G F))
x : G
h : MulSemiringAction.toAlgHom (↥(subfield G F)) F x = (↑f : F →ₐ[↥(subfield G F)] F)
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀
    (h :
      ∀ (x_1 : F),
        Eq (α := F) ((MulSemiringAction.toAlgHom (↥(subfield G F)) F x : (a : F) → F) x_1 : F)
          (((↑f : F →ₐ[↥(subfield G F)] F) : (a : F) → F) x_1 : F))
    (x_1 : F),
    Eq (α := F)
      (((((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
                  (a : G) → Gal(F/↥(subfield G F)))
                x :
              Gal(F/↥(subfield G F))) :
            (a : F) → F)
          x_1 :
        F)
      ((f : (a : F) → F) x_1 : F)
⊢ ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
        (a : G) → Gal(F/↥(subfield G F)))
      x =
    f

Tactic:
rwa [DFunLike.ext_iff] at h ⊢

Premises used: DFunLike.ext_iff
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
h : ∀ (g₁ g₂ : G), (∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a) → ⟦g₁⟧ = ⟦g₂⟧
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
g₁ g₂ : G
h : ∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a
h₁ : g₁⁻¹ * g₂ ∈ f.ker
h₂ :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield G F)))
    ((f : (a : G) → Gal(F/↥(subfield G F))) (g₁⁻¹ * g₂) : Gal(F/↥(subfield G F))) (1 : Gal(F/↥(subfield G F)))
h₃ :
  HMul.hMul (α := Gal(F/↥(subfield G F))) (β := Gal(F/↥(subfield G F)))
      ((f : (a : G) → Gal(F/↥(subfield G F))) g₁⁻¹ : Gal(F/↥(subfield G F)))
      ((f : (a : G) → Gal(F/↥(subfield G F))) g₂ : Gal(F/↥(subfield G F))) =
    1
h₄ :
  HMul.hMul (α := Gal(F/↥(subfield G F))) (β := Gal(F/↥(subfield G F)))
      (((f : (a : G) → Gal(F/↥(subfield G F))) g₁)⁻¹ : Gal(F/↥(subfield G F)))
      ((f : (a : G) → Gal(F/↥(subfield G F))) g₂ : Gal(F/↥(subfield G F))) =
    1
h₅ :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield G F))) ((f : (a : G) → Gal(F/↥(subfield G F))) g₁ : Gal(F/↥(subfield G F)))
    ((f : (a : G) → Gal(F/↥(subfield G F))) g₂ : Gal(F/↥(subfield G F)))
h₆ h₇ h₈ h₉ :
  ∀ (a : F),
    Eq (α := F) ((((f : (a : G) → Gal(F/↥(subfield G F))) g₁ : Gal(F/↥(subfield G F))) : (a : F) → F) a : F)
      ((((f : (a : G) → Gal(F/↥(subfield G F))) g₂ : Gal(F/↥(subfield G F))) : (a : F) → F) a : F)
⊢ ⟦g₁⟧ = ⟦g₂⟧

Tactic:
rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]

Premises used: map_inv, AlgEquiv.ext_iff, QuotientGroup.eq, MonoidHom.mem_ker, map_mul, inv_mul_eq_one
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
⊢ FaithfulSMul Q F

Tactic:
have : FaithfulSMul Q F := ⟨fun {q₁ q₂} ↦ by
    induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂
    intro h
    rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]⟩
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
obtain :
  ∀ (q : Q)
    (hq :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            q :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ∃ (a : G),
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
            (a : G) → Gal(F/↥(subfield G F)))
          a =
        f
⊢ ∃ (a : G),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        a =
      f

Tactic:
obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
    (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))

Premises used: Algebra.algebraMap, QuotientGroup.mk, Membership.mem, Subtype, _private.0.FixedPoints.toAlgAut_surjective.match_1, Subtype.mk, Function.Bijective.surjective, AlgEquiv.toRingEquiv, FixedPoints.subfield, FixedPoints.toAlgAut_bijective, AlgEquiv.ofRingEquiv, AlgEquiv.commutes', Eq, DFunLike.coe
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
hq :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
    (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
          (a : Q) → Gal(F/↥(subfield Q F)))
        q :
      Gal(F/↥(subfield Q F)))
    (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))
revert :
  ∀
    (hq :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            q :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ∃ (a : G),
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
            (a : G) → Gal(F/↥(subfield G F)))
          a =
        f
⊢ ∃ (a : G),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        a =
      f

Tactic:
revert hq
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
⊢ ∀
    (hq :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            q :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ∃ (a : G),
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
            (a : G) → Gal(F/↥(subfield G F)))
          a =
        f

Tactic:
QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
refine :
  ∀ (g : G)
    (hg :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            (↑g : G ⧸ f_1.ker) :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
          (a : G) → Gal(F/↥(subfield G F)))
        g =
      f
⊢ ∀
    (hq :
      Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
        (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
              (a : Q) → Gal(F/↥(subfield Q F)))
            q :
          Gal(F/↥(subfield Q F)))
        (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))),
    ∃ (a : G),
      ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
            (a : G) → Gal(F/↥(subfield G F)))
          a =
        f

Tactic:
refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u_2
F : Type u_3
inst : Group G
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Finite G
f_1 : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f_1.ker
x : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f_1)
this : FaithfulSMul Q F
f : Gal(F/↥(subfield G F))
q : Q
g : G
hg :
  Eq.{u_3 + 1} (α := Gal(F/↥(subfield Q F)))
    (((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
          (a : Q) → Gal(F/↥(subfield Q F)))
        (↑g : G ⧸ f_1.ker) :
      Gal(F/↥(subfield Q F)))
    (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : Gal(F/↥(subfield Q F)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hg :
      ∀ (a : F),
        Eq (α := F)
          (((((MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F : MonoidHom.{u_2, u_3} Q Gal(F/↥(subfield Q F))) :
                      (a : Q) → Gal(F/↥(subfield Q F)))
                    (↑g : G ⧸ f_1.ker) :
                  Gal(F/↥(subfield Q F))) :
                (a : F) → F)
              a :
            F)
          ((AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : (a : F) → F) a : F))
    (a : F),
    Eq (α := F)
      (((((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
                  (a : G) → Gal(F/↥(subfield G F)))
                g :
              Gal(F/↥(subfield G F))) :
            (a : F) → F)
          a :
        F)
      ((f : (a : F) → F) a : F)
⊢ ((MulSemiringAction.toAlgAut G (↥(subfield G F)) F : MonoidHom.{u_2, u_3} G Gal(F/↥(subfield G F))) :
        (a : G) → Gal(F/↥(subfield G F)))
      g =
    f

Tactic:
rwa [AlgEquiv.ext_iff] at hg ⊢

Premises used: AlgEquiv.ext_iff
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(L/K)
obtain :
  ∀ (x : Gal(M/K)),
    HMul.hMul (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K)) y =
      HMul.hMul (β := Gal(L/K)) y ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
⊢ x * y = y * x

Tactic:
obtain ⟨x, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M x

Premises used: AlgEquiv.restrictNormalHom_surjective, rfl
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
y : Gal(L/K)
x : Gal(M/K)
obtain :
  ∀ (y : Gal(M/K)),
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
        ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
      HMul.hMul (α := Gal(L/K)) (β := Gal(L/K))
        ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
        ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
⊢ HMul.hMul (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K)) y =
    HMul.hMul (β := Gal(L/K)) y ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))

Tactic:
obtain ⟨y, rfl⟩ := AlgEquiv.restrictNormalHom_surjective M y

Premises used: AlgEquiv.restrictNormalHom_surjective, rfl
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
rw :
  (AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
rw₁ :
  Eq.{u_2 + 1} (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (x * y) : Gal(L/K))
    ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
    ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) (y * x) : Gal(L/K))
⊢ HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K)) =
    HMul.hMul (α := Gal(L/K)) (β := Gal(L/K)) ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) y : Gal(L/K))
      ((AlgEquiv.restrictNormalHom L : (a : Gal(M/K)) → Gal(L/K)) x : Gal(L/K))

Tactic:
rw [← map_mul, ← map_mul, mul_comm]

Premises used: map_mul, mul_comm
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K M
⊢ IsAbelianGalois L M

Tactic:
have : IsGalois L M := .tower_top_of_isGalois K L M
  { is_comm.comm x y := AlgEquiv.restrictScalars_injective K
      (mul_comm (x.restrictScalars K) (y.restrictScalars K)) }

Premises used: IsGalois.tower_top_of_isGalois, IsAbelianGalois.mk
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
f : L →ₐ[K] M
inst_5 : IsAbelianGalois K M
⊢ IsAbelianGalois K L

Tactic:
letI := f.toRingHom.toAlgebra
  haveI := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
  .tower_bot K L M

Premises used: IsAbelianGalois.tower_bot
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
inst_7 : IsAbelianGalois K L
K' : IntermediateField K L
⊢ IsAbelianGalois.{u_1, u_2} K ↥K'

Tactic:
.tower_bot K K' L

Premises used: Membership.mem, Subtype, IsAbelianGalois.tower_bot
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K_1 : Type u_1
L_1 : Type u_2
M : Type u_3
inst : Field K_1
inst_1 : Field L_1
inst_2 : Algebra K_1 L_1
inst_3 : Field M
inst_4 : Algebra K_1 M
inst_5 : Algebra L_1 M
inst_6 : IsScalarTower K_1 L_1 M
K : Type u_4
L : Type u_5
inst_7 : Field K
inst_8 : Field L
inst_9 : Algebra K L
inst_10 : IsAbelianGalois K L
K' : IntermediateField K L
⊢ IsAbelianGalois (↥K') L

Tactic:
.tower_top K _ L

Premises used: IsAbelianGalois.tower_top
-- Module: Mathlib.FieldTheory.Galois.Abelian
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
⊢ IsAbelianGalois.{u_1, u_2} K ↥⊥

Tactic:
.of_algHom (IntermediateField.botEquiv K L).toAlgHom

Premises used: AlgEquiv.toAlgHom, IsAbelianGalois.of_algHom, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E

Tactic:
⟨fun h => ⟨h.1, h.2⟩, fun h =>
    { to_isSeparable := h.1
      to_normal := h.2 }⟩

Premises used: IsGalois.to_normal, IsGalois.mk, And.intro, Iff.intro, IsGalois.to_isSeparable
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ IsGalois F F

Tactic:
⟨⟩

Premises used: IsGalois.mk
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
x : E
⊢ IsIntegral F x

Tactic:
to_normal.isIntegral x

Premises used: IsGalois.to_normal, Normal.isIntegral
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
x : E
⊢ IsSeparable F x

Tactic:
Algebra.IsSeparable.isSeparable F x

Premises used: Algebra.IsSeparable.isSeparable
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
x : E
⊢ Polynomial.Splits (Polynomial.map (algebraMap F E) (minpoly F x))

Tactic:
Normal.splits' x

Premises used: Normal.splits'