awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ HSMul.hSMul (β := L) g ((algebraMap (FractionRing B) L : (a : FractionRing B) → L) x : L) =
    (algebraMap (FractionRing B) L : (a : FractionRing B) → L) x
have 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))
Tactic: obtain ⟨a, b, _, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ HSMul.hSMul (β := C) g ((algebraMap B C : (a : B) → C) x : C) = (algebraMap B C : (a : B) → C) x
have 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)
Tactic: apply FaithfulSMul.algebraMap_injective C L
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ 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)
have 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)
Tactic: rw [algebraMap.smul']
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ 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)
have 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)
Tactic: apply h
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use algebraMap B (FractionRing B) x
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ 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)
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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'
⊢ 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)
have hg : g⁻¹ * g' ∈ N
Tactic: rw [smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul, smul_eq_self G K L N]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) 1 x) : L) = (↑x : L)
have rw : (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) (↑1 : G ⧸ N) x) : L) = (↑x : L)
Tactic: rw [← QuotientGroup.mk_one, coe_quotient_smul, one_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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)
⊢ (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) 1 x) : L) = (↑x : L)
have rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := G) 1 (↑x : L) = (↑x : L)
Tactic: rw [← QuotientGroup.mk_one, coe_quotient_smul, one_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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)
⊢ (↑(HSMul.hSMul.{u_1, u_4, u_4} (α := G ⧸ N) 1 x) : L) = (↑x : L)
have rw₂ : (↑x : L) = (↑x : L)
Tactic: rw [← QuotientGroup.mk_one, coe_quotient_smul, one_smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
⊢ Eq (α := G ⧸ N) (Quotient.mk'' g₁) (Quotient.mk'' g₂)
have rw : ∀ y ∈ (↑F : Set L), (g₁⁻¹ * g₂) • y = y
Tactic: rw [QuotientGroup.eq, ← fixingSubgroup_fixedPoints G K L N, subgroup_iff.mp hF,
      mem_fixingSubgroup_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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₁⁻¹ * g₂) • x = x
have rw : g₂ • x = g₁ • x
Tactic: rw [mul_smul, inv_smul_eq_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x
have this : ∀ (g : G), g • (↑x : L) = (↑x : L)
Tactic: have : ∀ (g : G), g • (x : L) = x := fun g ↦ by
      simpa [coe_quotient_smul] using congr_arg Subtype.val (h g)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x
have obtain : ∀ (a : K) (ha : (algebraMap K L : (a : K) → L) a = (↑x : L)), ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x
Tactic: obtain ⟨a, ha⟩ := hK.isInvariant.isInvariant x this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
⊢ ∃ (a : K), (algebraMap K ↥F : (a : K) → ↥F) a = x
have refine : Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
  ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
Tactic: refine ⟨a, FaithfulSMul.algebraMap_injective F L ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw : Eq.{u_4 + 1} (α := L) ((algebraMap K L : (a : K) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
rw : Eq.{u_4 + 1} (α := L) ((algebraMap K L : (a : K) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw₁ : (↑x : L) = (algebraMap (↥F) L : (a : ↥F) → L) x
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
x : ↥F
h : ∀ (g : G ⧸ N), g • x = x
this : ∀ (g : G), g • (↑x : L) = (↑x : L)
a : K
ha : (algebraMap K L : (a : K) → L) a = (↑x : L)
rw : Eq.{u_4 + 1} (α := L) ((algebraMap K L : (a : K) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
rw₁ : (↑x : L) = (algebraMap (↥F) L : (a : ↥F) → L) x
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap K ↥F : (a : K) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw₂ : (↑x : L) = (↑x : L)
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h).toAlgebra
⊢ FaithfulSMul.{u_1, u_4} ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥F
have this₁ : FaithfulSMul.{u_1, u_4} (G ⧸ N) ↥F
Tactic: have := hFN.faithful
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h_1 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
⊢ ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x
have obtain : ∀ (a : ↥E) (ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)), ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x
Tactic: obtain ⟨a, ha⟩ := hE.isInvariant.isInvariant x
        fun ⟨g, hg⟩ ↦ congr_arg Subtype.val (h ⟨g, g, hg, rfl⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h_1 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
a : ↥E
ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)
⊢ ∃ (a : ↥E), (algebraMap ↥E ↥F : (a : ↥E) → ↥F) a = x
have this₁ : IsScalarTower (↥E) (↥F) L
Tactic: have : IsScalarTower E F L := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h_1 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this_1 : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
a : ↥E
ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)
this : IsScalarTower (↥E) (↥F) L
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap ↥E ↥F : (a : ↥E) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw : Eq (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
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
N : Subgroup G
inst_5 : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
hK : IsGaloisGroup G K L
inst_6 : Finite G
E : IntermediateField K L
hE : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥E) L
h_1 : E ≤ F
hFN : IsGaloisGroup.{u_1, u_3, u_4} (G ⧸ N) K ↥F
this_1 : Algebra ↥E ↥F := (IntermediateField.inclusion h_1).toAlgebra
x : ↥F
h : ∀ (g : ↥(Subgroup.map (QuotientGroup.mk' N) H)), g • x = x
a : ↥E
ha : (algebraMap (↥E) L : (a : ↥E) → L) a = (↑x : L)
this : IsScalarTower (↥E) (↥F) L
rw : Eq (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) a : L) ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
⊢ Eq (α := L) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap ↥E ↥F : (a : ↥E) → ↥F) a : ↥F) : L)
    ((algebraMap (↥F) L : (a : ↥F) → L) x : L)
have rw₁ : (↑x : L) = (algebraMap (↥F) L : (a : ↥F) → L) x
Tactic: rw [← IsScalarTower.algebraMap_apply, ha, IntermediateField.algebraMap_apply]