awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (∀ (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

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- 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
h₁ :
  (∀ (y : L),
      (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y) →
    ∀ (y : C), (∃ (y_1 : B), (algebraMap B C : (a : B) → C) y_1 = y) → g • y = y
⊢ (∀ (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

Tactic:
refine ⟨?_, ?_⟩
-- 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
x_1 : FractionRing B
x : B
rw :
  HSMul.hSMul (β := L) g ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L) =
    (algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x)
rw₁ :
  Eq (α := L) ((algebraMap C L : (a : C) → L) (HSMul.hSMul (β := C) g ((algebraMap B C : (a : B) → C) x : C)) : L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
rw₂ rw₃ :
  Eq (α := L) ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
⊢ HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
    ((algebraMap B L : B →+* L) : (a : B) → L) x

Tactic:
rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]

Premises used: Exists.intro, algebraMap.smul', IsScalarTower.algebraMap_apply, rfl
-- 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
x : FractionRing B
⊢ ∀ {x : B},
    HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
      ((algebraMap B L : B →+* L) : (a : B) → L) x

Tactic:
have {x} : g • (algebraMap B L) x = (algebraMap B L) x := by
      rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
-- 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_5 : 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
x : FractionRing B
this :
  ∀ {x : B},
    HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
      ((algebraMap B L : B →+* L) : (a : B) → L) x
h₁ :
  ∀ (a b : B),
    Membership.mem (γ := Submonoid B) (nonZeroDivisors B) b →
      HSMul.hSMul (β := L) g
          ((algebraMap (FractionRing B) L : (a : FractionRing B) → L)
              (HDiv.hDiv (α := FractionRing B) (β := FractionRing B)
                ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) a : FractionRing B)
                ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B)) :
            L) =
        (algebraMap (FractionRing B) L : (a : FractionRing B) → L)
          (HDiv.hDiv (α := FractionRing B) (β := FractionRing B)
            ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) a : FractionRing B)
            ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B))
⊢ HSMul.hSMul (β := L) g ((algebraMap (FractionRing B) L : (a : FractionRing B) → L) x : L) =
    (algebraMap (FractionRing B) L : (a : FractionRing B) → L) x

Tactic:
obtain ⟨a, b, _, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- 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_5 : 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
this :
  ∀ {x : B},
    HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
      ((algebraMap B L : B →+* L) : (a : B) → L) x
a b : B
left : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) b
⊢ HSMul.hSMul (β := L) g
      ((algebraMap (FractionRing B) L : (a : FractionRing B) → L)
          (HDiv.hDiv (α := FractionRing B) (β := FractionRing B)
            ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) a : FractionRing B)
            ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B)) :
        L) =
    (algebraMap (FractionRing B) L : (a : FractionRing B) → L)
      (HDiv.hDiv (α := FractionRing B) (β := FractionRing B)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) a : FractionRing B)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B))

Tactic:
simp only [map_div₀, ← IsScalarTower.algebraMap_apply, smul_div₀', this]

Premises used: map_div₀, smul_div₀', IsScalarTower.algebraMap_apply
-- 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 : L), (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
x : B
h₁ :
  Eq (α := L) ((algebraMap C L : (a : C) → L) (HSMul.hSMul (β := C) g ((algebraMap B C : (a : B) → C) x : C)) : L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
⊢ HSMul.hSMul (β := C) g ((algebraMap B C : (a : B) → C) x : C) = (algebraMap B C : (a : B) → C) x

Tactic:
apply FaithfulSMul.algebraMap_injective C L

Premises used: FaithfulSMul.algebraMap_injective
-- 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 : L), (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
x : B
h₁ :
  HSMul.hSMul (β := L) g ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L) =
    (algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x)
⊢ Eq (α := L) ((algebraMap C L : (a : C) → L) (HSMul.hSMul (β := C) g ((algebraMap B C : (a : B) → C) x : C)) : L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)

Tactic:
rw [algebraMap.smul']

Premises used: algebraMap.smul'
-- 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 : L), (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
x : B
h₁ :
  ∃ (y : FractionRing B),
    Eq.{u_7 + 1} (α := L) ((algebraMap (FractionRing B) L : (a : FractionRing B) → L) y : L)
      ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
⊢ HSMul.hSMul (β := L) g ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L) =
    (algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x)

Tactic:
apply h
-- 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 : L), (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
x : B
h₁ :
  Eq.{u_7 + 1} (α := L)
    ((algebraMap (FractionRing B) L : (a : FractionRing B) → L)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
⊢ ∃ (y : FractionRing B),
    Eq.{u_7 + 1} (α := L) ((algebraMap (FractionRing B) L : (a : FractionRing B) → L) y : L)
      ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)

Tactic:
use algebraMap B (FractionRing B) x

Premises used: Algebra.algebraMap, FractionRing, DFunLike.coe
-- 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 : L), (∃ (y_1 : FractionRing B), (algebraMap (FractionRing B) L : (a : FractionRing B) → L) y_1 = y) → g • y = y
x : B
h₁ :
  Eq.{u_7 + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)
h₂ h₃ :
  Eq.{u_7 + 1} (α := L) (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
    (((algebraMap B L : B →+* L) : (a : B) → L) x : L)
⊢ Eq.{u_7 + 1} (α := L)
    ((algebraMap (FractionRing B) L : (a : FractionRing B) → L)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      L)
    ((algebraMap C L : (a : C) → L) ((algebraMap B C : (a : B) → C) x) : L)

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
x : ↥F
g g' : G
h : (QuotientGroup.leftRel N : G → G → Prop) g g'
hg : g⁻¹ * g' ∈ N
⊢ Eq.{u_4 + 1} (α := L) (↑((fun (g : G) ↦ Subtype.mk (p := fun (x : L) ↦ x ∈ F) (g • (↑x : L)) ⋯) g) : L)
    (↑((fun (g : G) ↦ Subtype.mk (p := fun (x : L) ↦ x ∈ F) (g • (↑x : L)) ⋯) g') : L)

Tactic:
rw [smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul, smul_eq_self G K L N]

Premises used: smul_assoc, IsGaloisGroup.smul_eq_self, smul_eq_mul, smul_eq_iff_eq_inv_smul
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
x : ↥F
g g' : G
h hg hg₁ hg₂ hg₃ : (QuotientGroup.leftRel N : G → G → Prop) g g'
⊢ g⁻¹ * g' ∈ N

Tactic:
rwa [← QuotientGroup.leftRel_apply]

Premises used: QuotientGroup.leftRel_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
F : IntermediateField K L
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (↑g : G ⧸ N) x) : L) = g • (↑x : L)

Tactic:
rfl

Premises used: 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
H H' : Subgroup G
F F' : IntermediateField K L
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 g'_1 : G ⧸ N
x : ↥F
g g' : G
⊢ (↑(HMul.hMul (α := G ⧸ N) (Quotient.mk'' g) (Quotient.mk'' g') • x) : L) =
    (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) (HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g') x)) : L)

Tactic:
simp [← QuotientGroup.mk_mul, coe_quotient_smul, mul_smul]

Premises used: IsGaloisGroup.coe_quotient_smul, QuotientGroup.mk_mul, SemigroupAction.mul_smul
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
x : ↥F
rw : (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) (↑1 : G ⧸ N) x) : L) = (↑x : L)
rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := G) 1 (↑x : L) = (↑x : L)
rw₂ rw₃ : (↑x : L) = (↑x : L)
⊢ (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) 1 x) : L) = (↑x : L)

Tactic:
rw [← QuotientGroup.mk_one, coe_quotient_smul, one_smul]

Premises used: QuotientGroup.mk_one, one_smul, IsGaloisGroup.coe_quotient_smul
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
g : G
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (β := ↥F) (Quotient.mk'' g) 0) : L) = (↑0 : L)

Tactic:
simp
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
x y : ↥F
g : G
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) (x + y)) : L) =
    (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) x + HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) y) : L)

Tactic:
simp [smul_add]

Premises used: smul_add
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
g : G
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (β := ↥F) (Quotient.mk'' g) 1) : L) = (↑1 : L)

Tactic:
simp
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g_1 : G ⧸ N
x y : ↥F
g : G
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) (x * y)) : L) =
    (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) x * HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) y) : L)

Tactic:
simp [smul_mul']

Premises used: smul_mul'
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
inst_8 : SMulCommClass G K L
g_1 : G ⧸ N
k : K
x : ↥F
g : G
⊢ (↑(HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) (k • x)) : L) =
    (↑(k • HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g) x) : L)

Tactic:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
g₁_1 g₂_1 : G ⧸ N
g₁ g₂ : G
h : ∀ (a : ↥F), HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₁) a = HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₂) a
rw : ∀ y ∈ (↑F : Set L), (g₁⁻¹ * g₂) • y = y
⊢ Eq (α := G ⧸ N) (Quotient.mk'' g₁) (Quotient.mk'' g₂)

Tactic:
rw [QuotientGroup.eq, ← fixingSubgroup_fixedPoints G K L N, subgroup_iff.mp hF,
      mem_fixingSubgroup_iff]

Premises used: QuotientGroup.eq, IsGaloisGroup.fixingSubgroup_fixedPoints, IsGaloisGroup.subgroup_iff, Iff.mp, mem_fixingSubgroup_iff
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
g₁_1 g₂_1 : G ⧸ N
g₁ g₂ : G
h : ∀ (a : ↥F), HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₁) a = HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₂) a
x : L
hx : x ∈ (↑F : Set L)
rw : g₂ • x = g₁ • x
⊢ (g₁⁻¹ * g₂) • x = x

Tactic:
rw [mul_smul, inv_smul_eq_iff]

Premises used: inv_smul_eq_iff, SemigroupAction.mul_smul
-- 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
N : Subgroup G
inst_7 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_8 : Finite G
g₁_1 g₂_1 : G ⧸ N
g₁ g₂ : G
h : ∀ (a : ↥F), HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₁) a = HSMul.hSMul (α := G ⧸ N) (Quotient.mk'' g₂) a
x : L
hx : x ∈ (↑F : Set L)
⊢ g₂ • x = g₁ • x

Tactic:
simpa [eq_comm, coe_quotient_smul] using congr_arg Subtype.val <| h ⟨x, hx⟩

Premises used: eq_comm, Subtype.mk, congr_arg, IsGaloisGroup.coe_quotient_smul, Subtype.val