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 : SMulCommClass G K L
⊢ Eq (α := Subgroup G) (fixingSubgroup G (↑⊥ : Set L)) ⊤

Tactic:
simp [Subgroup.ext_iff, mem_fixingSubgroup_iff, IntermediateField.mem_bot]

Premises used: Subgroup.ext_iff, mem_fixingSubgroup_iff, IntermediateField.mem_bot
-- 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 : SMulCommClass G K L
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊥) ⊤

Tactic:
simp [IntermediateField.ext_iff]

Premises used: IntermediateField.ext_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
inst_5 : SMulCommClass G K L
⊢ F ≤ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H ↔ H ≤ fixingSubgroup G (↑F : Set L)

Tactic:
⟨fun h g hg x ↦ h x.2 ⟨g, hg⟩, fun h x hx g ↦ h g.2 ⟨x, hx⟩⟩

Premises used: Subtype.mk, Iff.intro, Subtype.property
-- 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 H' : Subgroup G
inst_5 : SMulCommClass G K L
h : H ≤ H'
⊢ LE.le.{u_4} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H')
    (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)

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

Premises used: Set.Mem, setOf, _private.0.IsGaloisGroup.fixedPoints_le_of_le.match_1, Subtype.mk, HSMul.hSMul, MulAction.fixedPoints, Eq
-- 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
hGKL : IsGaloisGroup G K L
⊢ FaithfulSMul G L

Tactic:
have := hGKL.faithful
-- 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
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
h : ∀ (x : G), Membership.mem (γ := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) x ↔ Membership.mem (γ := Subgroup G) ⊥ x
⊢ Eq (α := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) ⊥

Tactic:
ext
-- 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
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
x : G
⊢ Membership.mem (γ := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) x ↔ Membership.mem (γ := Subgroup G) ⊥ x

Tactic:
simpa [mem_fixingSubgroup_iff, Set.ext_iff] using MulAction.fixedBy_eq_univ_iff_eq_one

Premises used: Set.ext_iff, mem_fixingSubgroup_iff, MulAction.fixedBy_eq_univ_iff_eq_one
-- 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
hGKL : IsGaloisGroup G K L
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥

Tactic:
IsGaloisGroup.fixedPoints_eq_bot G K L

Premises used: IsGaloisGroup.fixedPoints_eq_bot
-- 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
hGKL : IsGaloisGroup G K L
h :
  Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤)
    (FixedPoints.intermediateField G)
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤) ⊥

Tactic:
convert! IsGaloisGroup.fixedPoints_eq_bot G K L

Premises used: IsGaloisGroup.fixedPoints_eq_bot
-- 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
hGKL : IsGaloisGroup G K L
h :
  ∀ (x : L),
    Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤) x ↔
      Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField G) x
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤)
    (FixedPoints.intermediateField G)

Tactic:
ext
-- 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
hGKL : IsGaloisGroup G K L
x : L
⊢ Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤) x ↔
    Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField G) x

Tactic:
simp
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
F : IntermediateField K L
⊢ Eq.{u_1 + 1} (α := (Subgroup G)ᵒᵈ)
    (((intermediateFieldEquivSubgroup G K L : OrderIso.{u_4, u_1} (IntermediateField K L) (Subgroup G)ᵒᵈ) :
          (a : IntermediateField K L) → (Subgroup G)ᵒᵈ)
        F :
      (Subgroup G)ᵒᵈ)
    ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) (fixingSubgroup G (↑F : Set L)) : (Subgroup G)ᵒᵈ)

Tactic:
rfl

Premises used: Set.Mem, fixingSubgroup, setOf, fixingSubmonoid, Set.preimage, Subgroup.comap, 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
F : IntermediateField K L
⊢ Eq.{u_1 + 1} (α := Subgroup G)
    ((OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G)
        (((intermediateFieldEquivSubgroup G K L : OrderIso.{u_4, u_1} (IntermediateField K L) (Subgroup G)ᵒᵈ) :
            (a : IntermediateField K L) → (Subgroup G)ᵒᵈ)
          F) :
      Subgroup G)
    (fixingSubgroup G (↑F : Set L) : Subgroup G)

Tactic:
rfl

Premises used: Set.Mem, fixingSubgroup, setOf, fixingSubmonoid, Set.preimage, Subgroup.comap, 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
H : (Subgroup G)ᵒᵈ
obtain :
  ∀ (H : Subgroup G),
    Eq.{u_4 + 1} (α := IntermediateField K L)
      (((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
              OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
            (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
          ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
        IntermediateField K L)
      (FixedPoints.intermediateField.{u_3, u_4, u_1}
          ↥((OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G)
                ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
              Subgroup G) :
        IntermediateField K L)
⊢ Eq.{u_4 + 1} (α := IntermediateField K L)
    (((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
            OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
          (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
        H :
      IntermediateField K L)
    (FixedPoints.intermediateField.{u_3, u_4, u_1}
        ↥((OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G) H : Subgroup G) :
      IntermediateField K L)

Tactic:
obtain ⟨H, rfl⟩ := OrderDual.toDual.surjective H

Premises used: OrderDual.toDual, Equiv.surjective, 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
H : Subgroup G
⊢ Eq.{u_4 + 1} (α := IntermediateField K L)
    (((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
            OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
          (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
        ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
      IntermediateField K L)
    (FixedPoints.intermediateField.{u_3, u_4, u_1}
        ↥((OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G)
              ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
            Subgroup G) :
      IntermediateField K L)

Tactic:
simp [IntermediateField.ext_iff, intermediateFieldEquivSubgroup,
    (mulEquivAlgEquiv G K L).surjective.forall, -mulEquivAlgEquiv_symm_apply]

Premises used: Function.Surjective.forall, IntermediateField.ext_iff, MulEquiv.surjective, IsGaloisGroup.mulEquivAlgEquiv, IsGaloisGroup.mulEquivAlgEquiv_symm_apply, IsGaloisGroup.intermediateFieldEquivSubgroup
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
H : Subgroup G
⊢ Eq.{u_4 + 1} (α := IntermediateField K L)
    (((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
            OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
          (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
        ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
      IntermediateField K L)
    (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H : IntermediateField K L)

Tactic:
intermediateFieldEquivSubgroup_symm_apply ..

Premises used: Set.Mem, IsGaloisGroup.intermediateFieldEquivSubgroup_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
H : Subgroup G
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
rw :
  fixingSubgroup G
      (↑(((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
                  OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
                (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
              ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) :
            IntermediateField K L) :
        Set L) =
    H
rw₁ :
  (OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G)
      (((intermediateFieldEquivSubgroup G K L : OrderIso.{u_4, u_1} (IntermediateField K L) (Subgroup G)ᵒᵈ) :
          (a : IntermediateField K L) → (Subgroup G)ᵒᵈ)
        (((OrderIso.symm (intermediateFieldEquivSubgroup G K L) :
              OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
            (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
          ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H))) =
    H
rw₂ :
  (OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G) ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) = H
rw₃ rw₄ : H = H
⊢ fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H

Tactic:
rw [← intermediateFieldEquivSubgroup_symm_apply_toDual,
    ← ofDual_intermediateFieldEquivSubgroup_apply,
    OrderIso.apply_symm_apply, OrderDual.ofDual_toDual]

Premises used: OrderIso.apply_symm_apply, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, OrderDual.ofDual_toDual, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
rw :
  FixedPoints.intermediateField.{u_3, u_4, u_1}
      ↥((OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G)
            (((intermediateFieldEquivSubgroup G K L : OrderIso.{u_4, u_1} (IntermediateField K L) (Subgroup G)ᵒᵈ) :
                (a : IntermediateField K L) → (Subgroup G)ᵒᵈ)
              F) :
          Subgroup G) =
    F
rw₁ :
  ((OrderIso.symm (intermediateFieldEquivSubgroup G K L) : OrderIso.{u_1, u_4} (Subgroup G)ᵒᵈ (IntermediateField K L)) :
        (a : (Subgroup G)ᵒᵈ) → IntermediateField K L)
      (((intermediateFieldEquivSubgroup G K L : OrderIso.{u_4, u_1} (IntermediateField K L) (Subgroup G)ᵒᵈ) :
          (a : IntermediateField K L) → (Subgroup G)ᵒᵈ)
        F) =
    F
rw₂ rw₃ : F = F
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥(fixingSubgroup G (↑F : Set L)) = F

Tactic:
rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_apply]

Premises used: IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, OrderIso.symm_apply_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
H : Subgroup G
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
h :
  ∀ (x : L),
    x ∈ (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) ↔
      Membership.mem (γ := Set L) (Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)) x
⊢ (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) =
    Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)

Tactic:
ext
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
x : L
h : (∀ (m : ↥H), m • x = x) ↔ ∃ (y : B), (algebraMap B L : (a : B) → L) y = x
⊢ x ∈ (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) ↔
    Membership.mem (γ := Set L) (Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)) x

Tactic:
rw [SetLike.mem_coe, FixedPoints.mem_intermediateField_iff, Set.mem_range]

Premises used: Set.mem_range, SetLike.mem_coe, FixedPoints.mem_intermediateField_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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
x : L
⊢ (∀ (m : ↥H), m • x = x) ↔ ∃ (y : B), (algebraMap B L : (a : B) → L) y = x

Tactic:
⟨IsGaloisGroup.isInvariant.isInvariant _, ?_⟩

Premises used: Algebra.IsInvariant.isInvariant, 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
x : L
h : (∃ (y : B), (algebraMap B L : (a : B) → L) y = x) → ∀ (m : ↥H), m • x = x
⊢ (∀ (m : ↥H), m • x = x) ↔ ∃ (y : B), (algebraMap B L : (a : B) → L) y = x

Tactic:
refine ⟨IsGaloisGroup.isInvariant.isInvariant _, ?_⟩
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
x : B
h : ↥H
⊢ HSMul.hSMul (β := L) h ((algebraMap B L : (a : B) → L) x : L) = (algebraMap B L : (a : B) → L) x

Tactic:
smul_algebraMap h x

Premises used: smul_algebraMap
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
x : B
h : ↥H
⊢ HSMul.hSMul (β := L) h ((algebraMap B L : (a : B) → L) x : L) = (algebraMap B L : (a : B) → L) x

Tactic:
exact smul_algebraMap h x

Premises used: smul_algebraMap
-- 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
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
B : Type u_5
inst_6 : CommSemiring B
inst_7 : Algebra B L
inst_8 : IsGaloisGroup.{u_1, u_5, u_4} (↥H) B L
rw : fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
rw₁ rw₂ : H = H
⊢ fixingSubgroup.{u_1, u_4} G (α := L) (Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)) = H

Tactic:
rw [← fixedPoints_eq_range_algebraMap G K L H, fixingSubgroup_fixedPoints]

Premises used: IsGaloisGroup.fixedPoints_eq_range_algebraMap, IsGaloisGroup.fixingSubgroup_fixedPoints
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
⊢ IsDomain B

Tactic:
have : IsDomain B := (FaithfulSMul.algebraMap_injective B C).isDomain
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this : IsDomain B
⊢ IsDomain A

Tactic:
have : IsDomain A := (FaithfulSMul.algebraMap_injective A C).isDomain
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this_1 : IsDomain B
this_2 : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
⊢ IsGaloisGroup G K L

Tactic:
have : IsGaloisGroup G K L := IsGaloisGroup.toFractionRing G A C
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this_1 : IsDomain B
this_2 : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this_3 : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
this : IsGaloisGroup G K L
⊢ IsGaloisGroup.{u_1, u_6, u_7} (↥H) (FractionRing B) L

Tactic:
have : IsGaloisGroup H (FractionRing B) L := IsGaloisGroup.toFractionRing H B C
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this_1 : IsDomain B
this_2 : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this_3 : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
this_4 : IsGaloisGroup G K L
this : IsGaloisGroup.{u_1, u_6, u_7} (↥H) (FractionRing B) L
rw :
  Eq (α := Subgroup G)
    (fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)))
    (fixingSubgroup.{u_1, u_7} G (α := L)
      (Set.range.{u_7, u_6 + 1} (ι := FractionRing B) (⇑(algebraMap (FractionRing B) L) : (a : FractionRing B) → L)))
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H

Tactic:
rw [← fixingSubgroup_range_algebraMap' G K L H (FractionRing B)]

Premises used: FractionRing, IsGaloisGroup.fixingSubgroup_range_algebraMap'
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this_1 : IsDomain B
this_2 : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this_3 : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
this_4 : IsGaloisGroup G K L
this : IsGaloisGroup.{u_1, u_6, u_7} (↥H) (FractionRing B) L
h :
  ∀ (g : G),
    Membership.mem (γ := Subgroup G)
        (fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C))) g ↔
      Membership.mem (γ := Subgroup G)
        (fixingSubgroup.{u_1, u_7} G (α := L)
          (Set.range.{u_7, u_6 + 1} (ι := FractionRing B)
            (⇑(algebraMap (FractionRing B) L) : (a : FractionRing B) → L)))
        g
⊢ Eq (α := Subgroup G)
    (fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)))
    (fixingSubgroup.{u_1, u_7} G (α := L)
      (Set.range.{u_7, u_6 + 1} (ι := FractionRing B) (⇑(algebraMap (FractionRing B) L) : (a : FractionRing B) → L)))

Tactic:
ext g
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
A : Type u_5
B : Type u_6
C : Type u_7
inst_2 : CommRing A
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra A C
inst_6 : FaithfulSMul A C
inst_7 : MulSemiringAction G C
H : Subgroup G
hGAC : IsGaloisGroup G A C
inst_8 : CommRing B
inst_9 : Algebra B C
inst_10 : FaithfulSMul B C
hH : IsGaloisGroup.{u_1, u_6, u_7} (↥H) B C
this_1 : IsDomain B
this_2 : IsDomain A
K : Type u_5 := FractionRing A
L : Type u_7 := FractionRing C
this_3 : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
this_4 : IsGaloisGroup G K L
this : IsGaloisGroup.{u_1, u_6, u_7} (↥H) (FractionRing B) L
g : G
h :
  (∀ (y : C), (∃ (y_1 : B), (algebraMap B C : (a : B) → C) y_1 = y) → g • y = y) ↔
    ∀ (y : L),
      (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
⊢ Membership.mem (γ := Subgroup G)
      (fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C))) g ↔
    Membership.mem (γ := Subgroup G)
      (fixingSubgroup.{u_1, u_7} G (α := L)
        (Set.range.{u_7, u_6 + 1} (ι := FractionRing B) (⇑(algebraMap (FractionRing B) L) : (a : FractionRing B) → L)))
      g

Tactic:
simp only [mem_fixingSubgroup_iff, Set.mem_range]

Premises used: Set.mem_range, mem_fixingSubgroup_iff