awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : IsDomain A
inst_6 : IsDomain B
inst_7 : IsTorsionFree A B
inst_8 : Finite G
inst_9 : IsGaloisGroup G A B
this : MulSemiringAction.{u_1, u_3} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
g : G
b : B
x : FractionRing B
⊢ g • b • x = (g • b) • g • x
have rw : HSMul.hSMul (β := FractionRing B) g ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B) *
    g • x =
  HMul.hMul (α := FractionRing B) ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) (g • b) : FractionRing B)
    (g • x)
Tactic: rw [Algebra.smul_def', Algebra.smul_def', smul_mul']
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : IsDomain A
inst_6 : IsDomain B
inst_7 : IsTorsionFree A B
inst_8 : Finite G
inst_9 : IsGaloisGroup G A B
this : MulSemiringAction.{u_1, u_3} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
g : G
b : B
x : FractionRing B
⊢ HSMul.hSMul (β := FractionRing B) g ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B) *
      g • x =
    HMul.hMul (α := FractionRing B)
      ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) (g • b) : FractionRing B) (g • x)
have e_a : HSMul.hSMul (β := FractionRing B) g ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) b : FractionRing B) =
  (algebraMap B (FractionRing B) : (a : B) → FractionRing B) (g • b)
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : IsDomain A
inst_6 : IsDomain B
inst_7 : IsTorsionFree A B
inst_8 : Finite G
inst_9 : IsGaloisGroup G A B
this : MulSemiringAction.{u_1, u_3} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
⊢ IsGaloisGroup.{u_1, u_2, u_3} G (FractionRing A) (FractionRing B)
have this₁ : SMulDistribClass G B (FractionRing B)
Tactic: have : SMulDistribClass G B (FractionRing B) := ⟨fun g b x ↦ by
    rw [Algebra.smul_def', Algebra.smul_def', smul_mul']
    congr
    exact IsFractionRing.fieldEquivOfAlgEquiv_algebraMap (FractionRing A) _ _ _ b⟩
-- 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
inst_5 : IsGaloisGroup G K L
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥
have rw : LE.le.{u_4} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥
Tactic: rw [eq_bot_iff]
-- 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
inst_5 : Finite G
inst_6 : IsGaloisGroup G K L
⊢ IsGalois K L
have rw : IsGalois (↥(FixedPoints.intermediateField G)) L
Tactic: rw [← isGalois_iff_isGalois_bot, ← fixedPoints_eq_bot G]
-- 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
inst_5 : IsGaloisGroup G K L
⊢ Nat.card G = finrank K L
have inl : ∀ (val : Fintype G), Nat.card G = finrank K L
Tactic: rcases fintypeOrInfinite G with _ | hG
-- 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
inst_5 : IsGaloisGroup G K L
inl : ∀ (val : Fintype G), Nat.card G = finrank K L
⊢ Nat.card G = finrank K L
have inr : ∀ (hG : Infinite G), Nat.card G = finrank K L
Tactic: rcases fintypeOrInfinite G with _ | hG
-- 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
inst_5 : IsGaloisGroup G K L
val : Fintype G
⊢ Nat.card G = finrank K L
have this : FaithfulSMul G L
Tactic: have : FaithfulSMul G L := faithful K
-- 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
inst_5 : IsGaloisGroup G K L
val : Fintype G
this : FaithfulSMul G L
⊢ Nat.card G = finrank K L
have inl : Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L
Tactic: rw [← IntermediateField.finrank_bot', ← fixedPoints_eq_bot G, Nat.card_eq_fintype_card]
-- 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
inst_5 : IsGaloisGroup G K L
hG : Infinite G
⊢ Nat.card G = finrank K L
have inr : finrank K L = 0
Tactic: rw [Nat.card_eq_zero_of_infinite, eq_comm]
-- 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
inst_5 : IsGaloisGroup G K L
hG : Infinite G
⊢ finrank K L = 0
have inr : ∀ (hG : finrank K L ≠ 0), Finite G
Tactic: contrapose! hG
Cleared hypotheses: hG
-- 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
inst_5 : IsGaloisGroup G K L
hG : finrank K L ≠ 0
⊢ Finite G
have this : FiniteDimensional K L
Tactic: have : FiniteDimensional K L := FiniteDimensional.of_finrank_pos (Nat.zero_lt_of_ne_zero hG)
-- 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
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
⊢ Function.Bijective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
    (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K))
have this : IsGalois K L
Tactic: have := isGalois G K L
-- 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
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this : IsGalois K L
⊢ Function.Bijective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
    (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K))
have this₁ : FiniteDimensional K L
Tactic: have := finiteDimensional G K 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
inst_7 : IsGaloisGroup G K L
inst_8 : Finite G
this_1 : IsGalois K L
this : FiniteDimensional K L
⊢ Function.Bijective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
    (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K))
have rw : Function.Injective.{u_1 + 1, u_4 + 1} (α := G) (β := Gal(L/K))
    (⇑(MulSemiringAction.toAlgAut G K L) : (a : G) → Gal(L/K)) ∧
  finrank K L = finrank K L
Tactic: rw [Nat.bijective_iff_injective_and_card, card_eq_finrank G K L,
      IsGalois.card_aut_eq_finrank K L]
-- 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
inst_5 : IsGaloisGroup G K L
inst_6 : Finite G
F : IntermediateField K L
⊢ Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L)) = F.fixingSubgroup
have h : ∀ (g : Gal(L/K)),
  Membership.mem (γ := Subgroup Gal(L/K))
      (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L))) g ↔
    g ∈ F.fixingSubgroup
Tactic: ext g
-- 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
inst_5 : IsGaloisGroup G K L
inst_6 : Finite G
F : IntermediateField K L
g : Gal(L/K)
⊢ Membership.mem (γ := Subgroup Gal(L/K))
      (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L))) g ↔
    g ∈ F.fixingSubgroup
have h : ∀ (g : G),
  Membership.mem (α := Gal(L/K)) (γ := Subgroup Gal(L/K))
      (Subgroup.map (↑(mulEquivAlgEquiv G K L) : G →* Gal(L/K)) (fixingSubgroup G (↑F : Set L)))
      (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K)) ↔
    Membership.mem (α := Gal(L/K)) F.fixingSubgroup
      (((mulEquivAlgEquiv G K L : MulEquiv.{u_1, u_4} G Gal(L/K)) : (a : G) → Gal(L/K)) g : Gal(L/K))
Tactic: obtain ⟨g, rfl⟩ := (mulEquivAlgEquiv G K L).surjective g
Cleared hypotheses: g
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F
have refine_1 : ∀ (x : L) (hx : Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x), x ∈ F
Tactic: refine IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x),
    x ∈ F
⊢ FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F
have refine_2 : ∀ (x : L) (hx : x ∈ F), Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
Tactic: refine IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
⊢ x ∈ F
have refine_1 : ∀ (a : ↥F)
  (hx :
    Membership.mem (α := L) (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H)
      ((algebraMap (↥F) L : (a : ↥F) → L) a : L)),
  Membership.mem (α := L) F ((algebraMap (↥F) L : (a : ↥F) → L) a : L)
Tactic: obtain ⟨a, rfl⟩ := hHFL.isInvariant.isInvariant x hx
Cleared hypotheses: x, hx
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
have this : Eq.{u_4 + 1} (α := IntermediateField K L)
  (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H))
  (IntermediateField.restrictScalars K (L' := ↥F) ⊥)
Tactic: have := congr_arg (restrictScalars K) <| IsGaloisGroup.fixedPoints_eq_bot H F L
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
this :
  Eq.{u_4 + 1} (α := IntermediateField K L)
    (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H))
    (IntermediateField.restrictScalars K (L' := ↥F) ⊥)
⊢ Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
have this₁ : IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F
Tactic: rw [restrictScalars_bot_eq_self] at this
Cleared hypotheses: this
-- 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
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
x : L
hx : x ∈ F
this : IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F
⊢ Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
have refine_2 : ∀
  (hx :
    Membership.mem (γ := IntermediateField K L)
      (IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H)) x)
  (this : IntermediateField.restrictScalars K (L' := ↥F) (FixedPoints.intermediateField.{u_4, u_4, u_1} ↥H) = F),
  Membership.mem (γ := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) x
Tactic: rwa [← this] at hx
Cleared hypotheses: hx, this
-- 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
hGKL : IsGaloisGroup G K L
hF : FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H = F
⊢ IsGaloisGroup.{u_1, u_4, u_4} (↥H) (↥F) L
have hF₁ : F = FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H
Tactic: rw [eq_comm] at hF
Cleared hypotheses: hF
-- 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
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
n : ↥N
⊢ n • g • (↑x : L) = g • (↑x : L)
have hg : g⁻¹ * (↑n : G) * g ∈ N
Tactic: rw [← smul_assoc, MulAction.subgroup_smul_def, smul_eq_mul,
      show n * g = g * (g⁻¹ * n * g) by group, ← smul_eq_mul, smul_assoc,
      IsGaloisGroup.smul_eq_self G K L N F (g⁻¹ * (n : G) * g)]
-- 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
F : IntermediateField K L
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
⊢ g • (↑x : L) ∈ F
have this : ∀ (n : ↥N), n • g • (↑x : L) = g • (↑x : L)
Tactic: have : ∀ (n : N), n • g • (x : L) = g • x := by
    intro n
    rw [← smul_assoc, MulAction.subgroup_smul_def, smul_eq_mul,
      show n * g = g * (g⁻¹ * n * g) by group, ← smul_eq_mul, smul_assoc,
      IsGaloisGroup.smul_eq_self G K L N F (g⁻¹ * (n : G) * g)]
    exact hN.conj_mem' n n.prop g
-- 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
N : Subgroup G
hN : N.Normal
hF : IsGaloisGroup.{u_1, u_4, u_4} (↥N) (↥F) L
g : G
x : ↥F
this : ∀ (n : ↥N), n • g • (↑x : L) = g • (↑x : L)
⊢ g • (↑x : L) ∈ F
have obtain : ∀ (y : ↥F) (hy : (algebraMap (↥F) L : (a : ↥F) → L) y = g • (↑x : L)), g • (↑x : L) ∈ F
Tactic: obtain ⟨y, hy⟩ := hF.isInvariant.isInvariant (g • x) this
-- 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
hGKL : IsGaloisGroup G K L
⊢ Eq (α := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) ⊥
have this : FaithfulSMul G L
Tactic: have := hGKL.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
hGKL : IsGaloisGroup G K L
this : FaithfulSMul G L
⊢ Eq (α := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) ⊥
have h : ∀ (x : G), Membership.mem (γ := Subgroup G) (fixingSubgroup G (↑⊤ : Set L)) x ↔ Membership.mem (γ := Subgroup G) ⊥ 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
hGKL : IsGaloisGroup G K L
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤) ⊥
have h : Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤)
  (FixedPoints.intermediateField G)
Tactic: convert! IsGaloisGroup.fixedPoints_eq_bot G K L
-- 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
hGKL : IsGaloisGroup G K L
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField.{u_3, u_4, u_1} ↥⊤)
    (FixedPoints.intermediateField G)
have 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
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
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)
        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)
have 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)
Tactic: obtain ⟨H, rfl⟩ := OrderDual.toDual.surjective H
Cleared hypotheses: H
-- 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
⊢ fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
have 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
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
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
⊢ fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
have 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
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
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
⊢ fixingSubgroup G (↑(FixedPoints.intermediateField.{u_3, u_4, u_1} ↥H) : Set L) = H
have rw₂ : (OrderDual.ofDual : (a : (Subgroup G)ᵒᵈ) → Subgroup G) ((OrderDual.toDual : (a : Subgroup G) → (Subgroup G)ᵒᵈ) H) = H
Tactic: rw [← intermediateFieldEquivSubgroup_symm_apply_toDual,
    ← ofDual_intermediateFieldEquivSubgroup_apply,
    OrderIso.apply_symm_apply, OrderDual.ofDual_toDual]