awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
have rw₃ : H = H
Tactic: rw [← intermediateFieldEquivSubgroup_symm_apply_toDual,
    ← ofDual_intermediateFieldEquivSubgroup_apply,
    OrderIso.apply_symm_apply, OrderDual.ofDual_toDual]
-- 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
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
inst_5 : Finite G
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥(fixingSubgroup G (↑F : Set L)) = F
have 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
Tactic: rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_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
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
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥(fixingSubgroup G (↑F : Set L)) = F
have 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
Tactic: rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_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
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
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥(fixingSubgroup G (↑F : Set L)) = F
have rw₂ : F = F
Tactic: rw [← ofDual_intermediateFieldEquivSubgroup_apply, ← intermediateFieldEquivSubgroup_symm_apply,
    OrderIso.symm_apply_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
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
⊢ (↑(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)
have 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
Tactic: ext
-- 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
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
⊢ 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
have h : (∀ (m : ↥H), m • x = x) ↔ ∃ (y : B), (algebraMap B L : (a : B) → L) y = x
Tactic: rw [SetLike.mem_coe, FixedPoints.mem_intermediateField_iff, Set.mem_range]
-- 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
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
have h : (∃ (y : B), (algebraMap B L : (a : B) → L) y = x) → ∀ (m : ↥H), m • x = x
Tactic: refine ⟨IsGaloisGroup.isInvariant.isInvariant _, ?_⟩
-- 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
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
⊢ fixingSubgroup.{u_1, u_4} G (α := L) (Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)) = H
have rw : fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
Tactic: rw [← fixedPoints_eq_range_algebraMap G K L H, fixingSubgroup_fixedPoints]
-- 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
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
⊢ fixingSubgroup.{u_1, u_4} G (α := L) (Set.range.{u_4, u_5 + 1} (ι := B) (⇑(algebraMap B L) : (a : B) → L)) = H
have rw₁ : H = H
Tactic: rw [← fixedPoints_eq_range_algebraMap G K L H, fixingSubgroup_fixedPoints]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H
have this : IsDomain B
Tactic: have : IsDomain B := (FaithfulSMul.algebraMap_injective B C).isDomain
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H
have this₁ : IsDomain A
Tactic: have : IsDomain A := (FaithfulSMul.algebraMap_injective A C).isDomain
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H
have this₁ : IsGaloisGroup G K L
Tactic: have : IsGaloisGroup G K L := IsGaloisGroup.toFractionRing G A C
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H
have this₁ : IsGaloisGroup.{u_1, u_6, u_7} (↥H) (FractionRing B) L
Tactic: have : IsGaloisGroup H (FractionRing B) L := IsGaloisGroup.toFractionRing H B C
-- 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
⊢ fixingSubgroup.{u_1, u_7} G (α := C) (Set.range.{u_7, u_6 + 1} (ι := B) (⇑(algebraMap B C) : (a : B) → C)) = H
have 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)))
Tactic: rw [← fixingSubgroup_range_algebraMap' G K L H (FractionRing B)]
-- 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
⊢ 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)))
have 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
Tactic: ext g
-- 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
⊢ 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
have 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
Tactic: simp only [mem_fixingSubgroup_iff, Set.mem_range]
-- 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
⊢ (∀ (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
have 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
Tactic: refine ⟨?_, ?_⟩
-- 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 : 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
⊢ (∀ (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
have 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
Tactic: refine ⟨?_, ?_⟩
-- 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 : C), (∃ (y_1 : B), (algebraMap B C : (a : B) → C) y_1 = y) → g • y = y
x_1 : 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
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
-- 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 : 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)
⊢ HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
    ((algebraMap B L : B →+* L) : (a : B) → L) x
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
-- 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 : 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)
⊢ HSMul.hSMul (β := L) g (((algebraMap B L : B →+* L) : (a : B) → L) x : L) =
    ((algebraMap B L : B →+* L) : (a : B) → L) x
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply B C L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
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
⊢ HSMul.hSMul (β := L) g ((algebraMap (FractionRing B) L : (a : FractionRing B) → L) x : L) =
    (algebraMap (FractionRing B) L : (a : FractionRing B) → L) x
have 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
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⟩]