awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
⊢ Polynomial.Splits
    (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))
have intro : ∀ (val : Fintype G),
  Polynomial.Splits
    (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ Polynomial.Splits
    (Polynomial.map (R := ↥(subfield G F)) (algebraMap (↥(subfield G F)) F) (_root_.minpoly (↥(subfield G F)) x))
have intro : Polynomial.Splits.{v} (R := F)
  (∏ g : G ⧸ stabilizer G x,
    HSub.hSub (α := Polynomial F) (β := Polynomial F) Polynomial.X
      ((Polynomial.C : (a : F) → Polynomial F) (ofQuotientStabilizer G x g) : Polynomial F))
Tactic: rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
      Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
⊢ IsSeparable (↥(subfield G F)) x
have intro : ∀ (val : Fintype G), IsSeparable (↥(subfield G F)) x
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
x : F
val : Fintype G
⊢ IsSeparable (↥(subfield G F)) x
have intro : Polynomial.Separable (prodXSubSMul G F x)
Tactic: rw [IsSeparable, ← minpoly_eq_minpoly,
      ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
      ← Subfield.toSubring_subtype_eq_subtype, Polynomial.map_toSubring _ (subfield G F).toSubring]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
inst_8 : Finite G
⊢ FiniteDimensional (↥(subfield G F)) F
have intro : ∀ (val : Fintype G), FiniteDimensional (↥(subfield G F)) F
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
inst_3 : Fintype G
⊢ finrank (↥(subfield G F)) F ≤ Fintype.card G
have rw : Module.rank (↥(subfield G F)) F ≤ (↑(Fintype.card G) : Cardinal.{v})
Tactic: rw [← @Nat.cast_le Cardinal, finrank_eq_rank]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
have intro : ∀ (val : Fintype G),
  Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
have intro : Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
  Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
Tactic: rw [Fintype.bijective_iff_injective_and_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
have intro : Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
  (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := G) (β := F →ₐ[↥(subfield G F)] F)
      (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
have intro₁ : Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
have intro : Fintype.card G ≤ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 G ≤ Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
⊢ Fintype.card G = Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F)
have intro₁ : Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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) ≤ Fintype.card G
have intro : Fintype.card.{u_3} (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F
Tactic: rw [← finrank_eq_card G F]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)))
have 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)
Tactic: refine ⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
    fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
⊢ 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)))
have 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
Tactic: refine ⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_,
    fun f ↦ ((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)))
⊢ Eq (α := F →ₐ[↥(subfield G F)] F) (MulSemiringAction.toAlgHom (↥(subfield G F)) F x)
    (MulSemiringAction.toAlgHom (↥(subfield G F)) F x_1)
have 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)
Tactic: rwa [DFunLike.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
⊢ ((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
have 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)
Tactic: rwa [DFunLike.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂
have h : ∀ (g₁ g₂ : G), (∀ (a : F), ⟦g₁⟧ • a = ⟦g₂⟧ • a) → ⟦g₁⟧ = ⟦g₂⟧
Tactic: induction q₁, q₂ using Quotient.inductionOn₂ with | _ g₁ g₂
Cleared hypotheses: q₁, q₂
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ ⟦g₁⟧ = ⟦g₂⟧
have h₁ : g₁⁻¹ * g₂ ∈ f.ker
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ ⟦g₁⟧ = ⟦g₂⟧
have 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)))
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)))
⊢ ⟦g₁⟧ = ⟦g₂⟧
have 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
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ ⟦g₁⟧ = ⟦g₂⟧
have 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
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ ⟦g₁⟧ = ⟦g₂⟧
have 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)))
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)))
⊢ ⟦g₁⟧ = ⟦g₂⟧
have 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)
Tactic: rwa [QuotientGroup.eq, MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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)
⊢ Function.Surjective.{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)))
have this : 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]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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))
⊢ ∃ (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
have 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) sorry : 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: obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
    (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
have 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) sorry : 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: revert hq
Cleared hypotheses: hq