awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
a : ⨆ (l : ↥L), f l ≤ L
⊢ ⨆ (l : ↥L), f l = L
have a₁ : L ≤ ⨆ (l : ↥L), f l
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
⊢ ⨆ (l : ↥L), f l ≤ L
have a : ∀ (i : ↥L), f i ≤ L
Tactic: apply iSup_le
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
l : K
hl : l ∈ L
⊢ Membership.mem (γ := IntermediateField k K) (⨆ (l : ↥L), f l) l
have a : l ∈ f (Subtype.mk (p := fun (x : K) ↦ x ∈ L) l hl)
Tactic: apply le_iSup f ⟨l, hl⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
⊢ IsGalois.{u_1, u_2} k ↥L
have this₁ : ⨆ (l : ↥L), f l = L
Tactic: have : (⨆ l : L, f l) = L := by
      apply le_antisymm
      · apply iSup_le
        intro l
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l.1}),
          fixedField_fixingSubgroup L] using inf_le_left
      · intro l hl
        apply le_iSup f ⟨l, hl⟩
        simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k {l}),
          fixedField_fixingSubgroup L, IntermediateField.mem_inf, hl, true_and]
          using adjoin_simple_le_iff.mp le_rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(toIntermediateField (adjoin k {x}))/k) :=
  fun (x : K) ↦ Subgroup.map (restrictNormalHom ↥(toIntermediateField (adjoin k {x}))) L.fixingSubgroup
f : (x : ↥L) → IntermediateField k K :=
  fun (x : ↥L) ↦
    IntermediateField.lift (F := toIntermediateField (adjoin k {(↑x : K)})) (IntermediateField.fixedField (g (↑x : K)))
this_1 : ∀ (x : K), (g x).Normal
this_2 : ∀ (l : ↥L), Normal.{u_1, u_2} k ↥(f l)
n : Normal.{u_1, u_2} k ↥(⨆ (l : ↥L), f l)
this : ⨆ (l : ↥L), f l = L
⊢ IsGalois.{u_1, u_2} k ↥L
have n₁ : Normal.{u_1, u_2} k ↥L
Tactic: rw [this] at n
Cleared hypotheses: n, this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
⊢ IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔
    FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L
have rw : FiniteDimensional.{u_1, u_2} k ↥L ∧ L.fixingSubgroup.Normal ↔
  FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L
Tactic: rw [isOpen_iff_finite, normal_iff_isGalois]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
rw :
  FiniteDimensional.{u_1, u_2} k ↥L ∧ L.fixingSubgroup.Normal ↔
    FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L
⊢ IsOpen L.fixingSubgroup.carrier ∧ L.fixingSubgroup.Normal ↔
    FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L
have rw₁ : FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L ↔
  FiniteDimensional.{u_1, u_2} k ↥L ∧ IsGalois.{u_1, u_2} k ↥L
Tactic: rw [isOpen_iff_finite, normal_iff_isGalois]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_4
inst : Group G
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra A B
inst_4 : MulSemiringAction G B
H : Type u_5
inst_5 : Group H
inst_6 : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) h : G) x = h • x
⊢ IsGaloisGroup H A B ↔ IsGaloisGroup G A B
have refine : ∀ (h : IsGaloisGroup H A B) (g : G) (x : B),
  HSMul.hSMul.{u_5, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x = g • x
Tactic: refine ⟨fun h ↦ h.of_mulEquiv e.symm fun g x ↦ ?_, fun h ↦ h.of_mulEquiv e he⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_4
inst : Group G
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra A B
inst_4 : MulSemiringAction G B
H : Type u_5
inst_5 : Group H
inst_6 : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) h : G) x = h • x
h : IsGaloisGroup H A B
g : G
x : B
⊢ HSMul.hSMul.{u_5, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x = g • x
have rw : HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x = g • x
Tactic: rw [← he, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_4
inst : Group G
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra A B
inst_4 : MulSemiringAction G B
H : Type u_5
inst_5 : Group H
inst_6 : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) h : G) x = h • x
h : IsGaloisGroup H A B
g : G
x : B
rw : HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) ((e.symm : (a : G) → H) g : H) : G) x = g • x
⊢ HSMul.hSMul.{u_5, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x = g • x
have rw₁ : g • x = g • x
Tactic: rw [← he, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst : Group G
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra A B
inst_4 : MulSemiringAction G B
inst_5 : FaithfulSMul A B
hA : IsGaloisGroup G A B
x : A
x_1 : G
⊢ HSMul.hSMul (β := B) x_1 ((algebraMap A B : (a : A) → B) x : B) = (algebraMap A B : (a : A) → B) x
have rw : Eq.{u_4 + 1} (α := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B)
Tactic: rw [smul_algebraMap]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
⊢ IsGaloisGroup G A B
have hc : ∀ (a : A),
  Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
Tactic: have hc (a : A) : (algebraMap K L) (algebraMap A K a) = (algebraMap B L) (algebraMap A B a) := by
    simp_rw [← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
⊢ IsGaloisGroup G A B
have refine_1 : ∀ {m₁ m₂ : G} (h : ∀ (a : B), m₁ • a = m₂ • a), m₁ = m₂
Tactic: refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
refine_1 : ∀ {m₁ m₂ : G} (h : ∀ (a : B), m₁ • a = m₂ • a), m₁ = m₂
⊢ IsGaloisGroup G A B
have refine_2 : ∀ (g : G) (x : A) (y : B),
  Eq.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) (g • x • y) : L)
    ((algebraMap B L : (a : B) → L) (x • g • y) : L)
Tactic: refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
refine_1 : ∀ {m₁ m₂ : G} (h : ∀ (a : B), m₁ • a = m₂ • a), m₁ = m₂
refine_2 :
  ∀ (g : G) (x : A) (y : B),
    Eq.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) (g • x • y) : L)
      ((algebraMap B L : (a : B) → L) (x • g • y) : L)
⊢ IsGaloisGroup G A B
have refine_3 : ∀ (x : B) (h : ∀ (g : G), g • x = x), ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
Tactic: refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
m₁ m₂ : G
h : ∀ (a : B), m₁ • a = m₂ • a
⊢ m₁ = m₂
have this : FaithfulSMul G L
Tactic: have := hGKL.faithful
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
m₁ m₂ : G
h : ∀ (a : B), m₁ • a = m₂ • a
this : FaithfulSMul G L
⊢ m₁ = m₂
have refine_1 : ∀ (y : L), m₁ • y = m₂ • y
Tactic: refine eq_of_smul_eq_smul fun (y : L) ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
m₁ m₂ : G
h : ∀ (a : B), m₁ • a = m₂ • a
this : FaithfulSMul G L
y : L
⊢ m₁ • y = m₂ • y
have refine_1 : ∀ (a b : B) (hb : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) b),
  m₁ • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) a : L) ((algebraMap B L : (a : B) → L) b : L) =
    m₂ • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) a : L) ((algebraMap B L : (a : B) → L) b : L)
Tactic: obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective B y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
have refine_3 : ∀ (b : K) (hb : Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) b : L) ((algebraMap B L : (a : B) → L) x : L)),
  ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
Tactic: obtain ⟨b, hb⟩ := hGKL.isInvariant.isInvariant (algebraMap B L x)
      (by simpa [← algebraMap.coe_smul'])
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
b : K
hb : Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) b : L) ((algebraMap B L : (a : B) → L) x : L)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
have hx : IsIntegral.{u_2, u_5} A (A := L) ((algebraMap B L : (a : B) → L) x : L)
Tactic: have hx : IsIntegral A (algebraMap B L x) := (Algebra.IsIntegral.isIntegral x).algebraMap
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (hypothesis)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
b : K
hb : Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) b : L) ((algebraMap B L : (a : B) → L) x : L)
hx : IsIntegral.{u_2, u_5} A (A := L) ((algebraMap B L : (a : B) → L) x : L)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
have hx₁ : ∃ (y : A), (algebraMap A K : (a : A) → K) y = b
Tactic: rw [← hb, isIntegral_algebraMap_iff (algebraMap K L).injective,
      IsIntegrallyClosedIn.isIntegral_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
b : K
hb : Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) b : L) ((algebraMap B L : (a : B) → L) x : L)
hx : ∃ (y : A), (algebraMap A K : (a : A) → K) y = b
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
have refine_3 : ∀ (a : A)
  (hb :
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) x : L)),
  ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
Tactic: obtain ⟨a, rfl⟩ := hx
Cleared hypotheses: b, hb, hx
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
a : A
hb :
  Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) x : L)
⊢ (algebraMap A B : (a : A) → B) a = x
have rwa : ∀
  (hb :
    Eq.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
      ((algebraMap B L : (a : B) → L) x : L)),
  (algebraMap A B : (a : A) → B) a = x
Tactic: rwa [hc, IsFractionRing.coe_inj] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.IsGaloisGroup (goal)
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
hGKL : IsGaloisGroup G K L
inst_17 : IsIntegrallyClosed A
inst_18 : Algebra.IsIntegral A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
x : B
h : ∀ (g : G), g • x = x
a : A
hb :
  Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) x : L)
rwa :
  ∀
    (hb :
      Eq.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
        ((algebraMap B L : (a : B) → L) x : L)),
    (algebraMap A B : (a : A) → B) a = x
⊢ (algebraMap A B : (a : A) → B) a = x
have rwa₁ : ∀ (hb : (algebraMap A B : (a : A) → B) a = x), (algebraMap A B : (a : A) → B) a = x
Tactic: rwa [hc, IsFractionRing.coe_inj] at hb
Cleared hypotheses: hb