awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
hG : Infinite G
inr : ∀ (hG : finrank K L ≠ 0), Finite G
⊢ finrank K L = 0

Tactic:
contrapose! hG
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
hG : finrank K L ≠ 0
⊢ FiniteDimensional K L

Tactic:
have : FiniteDimensional K L := FiniteDimensional.of_finrank_pos (Nat.zero_lt_of_ne_zero hG)
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
hG : finrank K L ≠ 0
this : FiniteDimensional K L
⊢ Finite G

Tactic:
Finite.of_injective (MulSemiringAction.toAlgAut G K L)
      (fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, Function.comp, DFunLike.ext_iff, MulSemiringAction.toAlgAut, Iff.mp, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
hG : finrank K L ≠ 0
this : FiniteDimensional K L
⊢ Finite G

Tactic:
exact Finite.of_injective (MulSemiringAction.toAlgAut G K L)
      (fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp)

Premises used: FaithfulSMul.eq_of_smul_eq_smul, Function.comp, DFunLike.ext_iff, MulSemiringAction.toAlgAut, Iff.mp, DFunLike.coe, Finite.of_injective
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : Finite G
inst_6 : IsGaloisGroup G K L
⊢ FiniteDimensional K L

Tactic:
FiniteDimensional.of_finrank_pos (card_eq_finrank G K L ▸ Nat.card_pos)

Premises used: Nat.card_pos, FiniteDimensional.of_finrank_pos, Eq.rec, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : FiniteDimensional K L
inst_6 : IsGaloisGroup G K L
⊢ Finite G

Tactic:
Nat.finite_of_card_ne_zero (card_eq_finrank G K L ▸ Module.finrank_pos.ne')

Premises used: Eq.rec, LT.lt.ne', IsGaloisGroup.card_eq_finrank, Nat.finite_of_card_ne_zero, Eq.symm, Module.finrank_pos
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
⊢ IsGalois K L

Tactic:
have := isGalois G K L
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this : IsGalois K L
⊢ FiniteDimensional K L

Tactic:
have := finiteDimensional G K L
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this_1 : IsGalois K L
this : FiniteDimensional K L
rw :
  Function.Injective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
      (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K)) ∧
    finrank K L = finrank K L
⊢ Function.Bijective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
    (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K))

Tactic:
rw [Nat.bijective_iff_injective_and_card, card_eq_finrank G K L,
      IsGalois.card_aut_eq_finrank K L]

Premises used: IsGalois.card_aut_eq_finrank, Nat.bijective_iff_injective_and_card, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this_1 : IsGalois K L
this : FiniteDimensional K L
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
      (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K)) ∧
    finrank K L = finrank K L

Tactic:
⟨fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp, rfl⟩

Premises used: FaithfulSMul.eq_of_smul_eq_smul, Function.comp, DFunLike.ext_iff, And.intro, Iff.mp, rfl
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this_1 : IsGalois K L
this : FiniteDimensional K L
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
      (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K)) ∧
    finrank K L = finrank K L

Tactic:
exact ⟨fun _ _ ↦ (faithful K).eq_of_smul_eq_smul ∘ DFunLike.ext_iff.mp, rfl⟩
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
inst_9 : IsGaloisGroup G' K L
inst_10 : Finite G'
g : G
x : L
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := G') ((mulEquivCongr G G' K L : (a : G) → G') g : G') x = g • x

Tactic:
AlgEquiv.ext_iff.mp ((mulEquivAlgEquiv G' K L).apply_symm_apply (mulEquivAlgEquiv G K L g)) x

Premises used: AlgEquiv.ext_iff, Function.surjInv, IsGaloisGroup.mulEquivAlgEquiv, Iff.mp, Classical.choose, DFunLike.coe, MulEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
inst_6 : Finite G
F : IntermediateField K L
h :
  ∀ (g : Gal(L/K)),
    Membership.mem (γ := Subgroup Gal(L/K))
        (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L))) g ↔
      g ∈ F.fixingSubgroup
⊢ Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L)) = F.fixingSubgroup

Tactic:
ext g
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
inst_6 : Finite G
F : IntermediateField K L
g : Gal(L/K)
h :
  ∀ (g : G),
    Membership.mem (α := Gal(L/K)) (γ := Subgroup Gal(L/K))
        (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L)))
        (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K)) ↔
      Membership.mem (α := Gal(L/K)) F.fixingSubgroup
        (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K))
⊢ Membership.mem (γ := Subgroup Gal(L/K))
      (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L))) g ↔
    g ∈ F.fixingSubgroup

Tactic:
obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g

Premises used: MulEquiv.surjective, IsGaloisGroup.mulEquivAlgEquiv, rfl
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGaloisGroup G K L
inst_6 : Finite G
F : IntermediateField K L
g : G
⊢ Membership.mem (α := Gal(L/K)) (γ := Subgroup Gal(L/K))
      (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L)))
      (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K)) ↔
    Membership.mem (α := Gal(L/K)) F.fixingSubgroup
      (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K))

Tactic:
simp [mem_fixingSubgroup_iff]

Premises used: mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F

Tactic:
IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.mpr, IntermediateField.ext_iff, Iff.intro
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x),
    x ∈ F
refine_2 :
  ∀ (x : L) (hx : x ∈ F),
    Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F

Tactic:
refine IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.mpr, IntermediateField.ext_iff, Iff.intro
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
refine_1 :
  ∀ (a : ↥F)
    (hx :
      Membership.mem (α := L) (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)
        ((algebraMap (↥F) L : (a : ↥F) → L) a : L)),
    Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) a : L)
⊢ x ∈ F

Tactic:
obtain ⟨a, rfl⟩ := hHFL.isInvariant.isInvariant x hx

Premises used: Algebra.IsInvariant.isInvariant, rfl
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
a : ↥F
hx :
  Membership.mem (α := L) (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)
    ((algebraMap (↥F) L : (a : ↥F) → L) a : L)
⊢ Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) a : L)

Tactic:
a.prop

Premises used: Set.Mem, Subtype.prop
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
a : ↥F
hx :
  Membership.mem (α := L) (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)
    ((algebraMap (↥F) L : (a : ↥F) → L) a : L)
⊢ Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) a : L)

Tactic:
exact a.prop

Premises used: Subtype.prop
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ Eq.{u_4 + 1} (α := IntermediateField K L)
    (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H))
    (IntermediateField.restrictScalars K (L' := ↥F) ⊥)

Tactic:
have := congr_arg (restrictScalars K) <| IsGaloisGroup.fixedPoints_eq_bot H F L
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
this :
  Eq.{u_4 + 1} (α := IntermediateField K L)
    (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H))
    (IntermediateField.restrictScalars K (L' := ↥F) ⊥)
⊢ IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F

Tactic:
rw [restrictScalars_bot_eq_self] at this

Premises used: IntermediateField.restrictScalars_bot_eq_self
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
this : IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀
    (hx :
      Membership.mem (γ := IntermediateField K L)
        (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H)) x)
    (this : IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F),
    Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
⊢ Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x

Tactic:
rwa [← this] at hx
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hF : FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F
⊢ F = FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H

Tactic:
rw [eq_comm] at hF

Premises used: eq_comm
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hF : F = FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H
⊢ IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)) L

Tactic:
IsGaloisGroup.subgroup G K L H

Premises used: IsGaloisGroup.subgroup
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hF : F = FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H
⊢ IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L

Tactic:
convert! IsGaloisGroup.subgroup G K L H

Premises used: IsGaloisGroup.subgroup
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
⊢ IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L ↔ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F

Tactic:
⟨fun _ ↦ fixedPoints_of_isGaloisGroup G K L H F, fun h ↦ of_fixedPoints_eq G K L H F h⟩

Premises used: IsGaloisGroup.fixedPoints_of_isGaloisGroup, IsGaloisGroup.of_fixedPoints_eq, Iff.intro
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
F : IntermediateField K L
inst_5 : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
g : G
hg : g ∈ H
x : ↥F
⊢ g • (↑x : L) = (↑x : L)

Tactic:
smul_algebraMap (⟨g, hg⟩ : H) x

Premises used: smul_algebraMap, Subtype.mk
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
n : ↥N
⊢ (↑n : G) * g = g * (g⁻¹ * (↑n : G) * g)

Tactic:
group
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
n : ↥N
hg : g⁻¹ * (↑n : G) * g ∈ N
⊢ n • g • (↑x : L) = g • (↑x : L)

Tactic:
rw [← smul_assoc, MulAction.subgroup_smul_def, smul_eq_mul,
      show n * g = g * (g⁻¹ * n * g) by group, ← smul_eq_mul, smul_assoc,
      IsGaloisGroup.smul_eq_self G K L N F (g⁻¹ * (n : G) * g)]

Premises used: HMul.hMul, smul_assoc, Inv.inv, IsGaloisGroup.smul_eq_self, MulAction.subgroup_smul_def, smul_eq_mul, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
n : ↥N
⊢ g⁻¹ * (↑n : G) * g ∈ N

Tactic:
hN.conj_mem' n n.prop g

Premises used: Subtype.prop, Subtype.val, Subgroup.Normal.conj_mem'
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
n : ↥N
⊢ g⁻¹ * (↑n : G) * g ∈ N

Tactic:
exact hN.conj_mem' n n.prop g

Premises used: Subtype.prop, Subtype.val, Subgroup.Normal.conj_mem'
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
⊢ ∀ (n : ↥N), n • g • (↑x : L) = g • (↑x : L)

Tactic:
have : ∀ (n : N), n • g • (x : L) = g • x := by
    intro n
    rw [← smul_assoc, MulAction.subgroup_smul_def, smul_eq_mul,
      show n * g = g * (g⁻¹ * n * g) by group, ← smul_eq_mul, smul_assoc,
      IsGaloisGroup.smul_eq_self G K L N F (g⁻¹ * (n : G) * g)]
    exact hN.conj_mem' n n.prop g
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
this : ∀ (n : ↥N), n • g • (↑x : L) = g • (↑x : L)
obtain : ∀ (y : ↥F) (hy : (algebraMap (↥F) L : (a : ↥F) → L) y = g • (↑x : L)), g • (↑x : L) ∈ F
⊢ g • (↑x : L) ∈ F

Tactic:
obtain ⟨y, hy⟩ := hF.isInvariant.isInvariant (g • x) this

Premises used: Algebra.IsInvariant.isInvariant, HSMul.hSMul, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
this : ∀ (n : ↥N), n • g • (↑x : L) = g • (↑x : L)
y : ↥F
hy : (algebraMap (↥F) L : (a : ↥F) → L) y = g • (↑x : L)
⊢ g • (↑x : L) ∈ F

Tactic:
simp [← hy]
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
H : Subgroup G
inst_5 : IsGaloisGroup G K L
⊢ finrank (↥(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)) L = Nat.card.{u_1} ↥H

Tactic:
(card_eq_finrank H (FixedPoints.intermediateField H) L).symm

Premises used: FixedPoints.intermediateField, Set.Mem, Membership.mem, Subtype, IsGaloisGroup.card_eq_finrank, Eq.symm
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
inst_5 : IsGalois K L
e : MulEquiv.{u_1, u_4} G Gal(L/K)
he : ∀ (g : G) (x : L), (((e : (a : G) → Gal(L/K)) g : Gal(L/K)) : (a : L) → L) x = g • x
⊢ IsGaloisGroup G K L

Tactic:
.of_mulEquiv e he

Premises used: IsGaloisGroup.of_mulEquiv
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
inst_7 : Finite G
inst_8 : FaithfulSMul G L
⊢ IsGaloisGroup G (↥(FixedPoints.subfield G L)) L

Tactic:
of_mulEquiv_algEquiv (FixedPoints.toAlgAutMulEquiv _ _) fun _ _ ↦ rfl

Premises used: IsGaloisGroup.of_mulEquiv_algEquiv, rfl, FixedPoints.toAlgAutMulEquiv
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
G' : Type u_2
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Group G'
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : MulSemiringAction G L
inst_6 : MulSemiringAction G' L
H H' : Subgroup G
F F' : IntermediateField K L
inst_7 : Finite G
hGKL : IsGaloisGroup G K L
⊢ IsGaloisGroup.{u_1, u_4, u_4} (↥(fixingSubgroup G (↑F : Set L))) (↥F) L

Tactic:
let e := ((mulEquivAlgEquiv G K L).subgroupMap (fixingSubgroup G (F : Set L))).trans <|
    (MulEquiv.subgroupCongr (map_mulEquivAlgEquiv_fixingSubgroup ..)).trans <|
    IntermediateField.fixingSubgroupEquiv F
  have := hGKL.isGalois
  .of_mulEquiv_algEquiv e fun _ _ ↦ rfl

Premises used: IsGaloisGroup.isGalois, Set.Mem, fixingSubgroup, MulEquiv.trans, MulEquiv.subgroupMap, MulEquiv.subgroupCongr, IntermediateField.fixingSubgroupEquiv, IsGaloisGroup.of_mulEquiv_algEquiv, SetLike.coe, IsGaloisGroup.mulEquivAlgEquiv, rfl, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F : IntermediateField K L
inst_5 : Finite G
inst_6 : IsGaloisGroup G K L
⊢ Nat.card.{u_1} ↥(fixingSubgroup G (↑F : Set L)) = finrank (↥F) L

Tactic:
card_eq_finrank ..

Premises used: Set.Mem, IsGaloisGroup.card_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
K : Type u_3
L : Type u_4
inst : Group G
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : MulSemiringAction G L
F F' : IntermediateField K L
h : F ≤ F'
⊢ LE.le (α := Subgroup G) (fixingSubgroup G (↑F' : Set L)) (fixingSubgroup G (↑F : Set L))

Tactic:
fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h hx⟩

Premises used: Set.Mem, setOf, Subtype.mk, _private.0.IsGaloisGroup.fixingSubgroup_le_of_le.match_1, HSMul.hSMul, Subtype.val, Eq