awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Infinite
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

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
-- Module: Mathlib.FieldTheory.Galois.Infinite
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
⊢ Normal.{u_1, u_2} k ↥L

Tactic:
rw [this] at n
-- Module: Mathlib.FieldTheory.Galois.Infinite
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
n₁ : Normal.{u_1, u_2} k ↥L
⊢ ⨆ (l : ↥L), f l = L

Tactic:
rw [this] at n
-- Module: Mathlib.FieldTheory.Galois.Infinite
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
this : ⨆ (l : ↥L), f l = L
⊢ IsGalois.{u_1, u_2} k ↥L

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Galois.Infinite
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 : IsGalois.{u_1, u_2} k ↥L
⊢ L.fixingSubgroup.Normal

Tactic:
simpa only [IntermediateFieldEquivClosedSubgroup, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
      ← L.restrictNormalHom_ker] using MonoidHom.normal_ker (restrictNormalHom L)

Premises used: Membership.mem, Subtype, InfiniteGalois.IntermediateFieldEquivClosedSubgroup, AlgEquiv.restrictNormalHom, MonoidHom.normal_ker, Equiv.coe_fn_mk, IntermediateField.restrictNormalHom_ker, RelIso.coe_fn_mk
-- Module: Mathlib.FieldTheory.Galois.Infinite
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
rw₁ 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
⊢ IsOpen L.fixingSubgroup.carrier ∧ 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]

Premises used: InfiniteGalois.normal_iff_isGalois, InfiniteGalois.isOpen_iff_finite
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
hG : IsGaloisGroup G A 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
m₁ m₂ : H
h : ∀ (a : B), m₁ • a = m₂ • a
⊢ ∀ (a : B),
    HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) m₁ : G) a =
      HSMul.hSMul.{u_1, u_4, u_4} (α := G) ((e : (a : H) → G) m₂ : G) a

Tactic:
simpa only [he]
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
hG : IsGaloisGroup G A 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
x : H
a : A
b : B
⊢ x • a • b = a • x • b

Tactic:
simpa [he] using hG.commutes.smul_comm (e x) a b

Premises used: SMulCommClass.smul_comm, DFunLike.coe
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
hG : IsGaloisGroup G A 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
b : B
h : ∀ (g : H), g • b = 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:
simp [← he]
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
hG : IsGaloisGroup G A 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
b : B
h : ∀ (g : H), g • b = b
he' : ∀ (g : G) (x : B), HSMul.hSMul.{u_5, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x = g • x
g : G
⊢ g • b = b

Tactic:
simpa [he'] using h (e.symm g)

Premises used: MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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

Tactic:
⟨fun h ↦ h.of_mulEquiv e.symm fun g x ↦ ?_, fun h ↦ h.of_mulEquiv e he⟩

Premises used: IsGaloisGroup.of_mulEquiv, Iff.intro, MulEquiv.symm
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
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
⊢ IsGaloisGroup H A B ↔ IsGaloisGroup G A B

Tactic:
refine ⟨fun h ↦ h.of_mulEquiv e.symm fun g x ↦ ?_, fun h ↦ h.of_mulEquiv e he⟩
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
rw₁ rw₂ : g • x = g • x
⊢ HSMul.hSMul.{u_5, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x = g • x

Tactic:
rw [← he, e.apply_symm_apply]

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ IsGaloisGroup.{u_1, u_2, u_4} (↥⊤) A B ↔ IsGaloisGroup G A B

Tactic:
iff_of_mulEquiv Subgroup.topEquiv fun _ _ ↦ rfl

Premises used: Subgroup.topEquiv, rfl, IsGaloisGroup.iff_of_mulEquiv
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : IsGaloisGroup G A B
⊢ IsGaloisGroup.{u_1, u_2, u_4} (↥⊤) A B

Tactic:
IsGaloisGroup.top_iff.mpr ‹_›

Premises used: Iff.mpr, IsGaloisGroup.top_iff
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
rw rw₁ : Eq.{u_4 + 1} (α := B) ((algebraMap A B : (a : A) → B) x : B) ((algebraMap A B : (a : A) → B) x : B)
⊢ HSMul.hSMul (β := B) x_1 ((algebraMap A B : (a : A) → B) x : B) = (algebraMap A B : (a : A) → B) x

Tactic:
rw [smul_algebraMap]

Premises used: smul_algebraMap
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ (fun (x : ↥(FixedPoints.subsemiring B G)) ↦
        (Exists.choose (p := fun (a : A) ↦ (algebraMap A B : (a : A) → B) a = (↑x : B)) ⋯ : A))
      ((fun (x : A) ↦
          (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
              ((algebraMap A B : (a : A) → B) x) ⋯ :
            ↥(FixedPoints.subsemiring B G)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 : ↥(FixedPoints.subsemiring B G)
⊢ (fun (x : A) ↦
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
            ((algebraMap A B : (a : A) → B) x) ⋯ :
          ↥(FixedPoints.subsemiring B G)))
      ((fun (x : ↥(FixedPoints.subsemiring B G)) ↦
          (Exists.choose (p := fun (a : A) ↦ (algebraMap A B : (a : A) → B) a = (↑x : B)) ⋯ : A))
        x) =
    x

Tactic:
simpa [Subtype.ext_iff] using (hA.isInvariant.isInvariant x x.prop).choose_spec

Premises used: Exists.choose_spec, Subtype.ext_iff, Algebra.IsInvariant.isInvariant, Subtype.prop, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 x_1 : A
⊢ Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
      ((algebraMap A B : (a : A) → B) (x * x_1)) ⋯ =
    HMul.hMul (α := ↥(FixedPoints.subsemiring B G)) (β := ↥(FixedPoints.subsemiring B G))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
          ((algebraMap A B : (a : A) → B) x) ⋯ :
        ↥(FixedPoints.subsemiring B G))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
          ((algebraMap A B : (a : A) → B) x_1) ⋯ :
        ↥(FixedPoints.subsemiring B G))

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 x_1 : A
⊢ Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
      ((algebraMap A B : (a : A) → B) (x + x_1)) ⋯ =
    HAdd.hAdd (α := ↥(FixedPoints.subsemiring B G)) (β := ↥(FixedPoints.subsemiring B G))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
          ((algebraMap A B : (a : A) → B) x) ⋯ :
        ↥(FixedPoints.subsemiring B G))
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subsemiring B) (FixedPoints.subsemiring B G) x)
          ((algebraMap A B : (a : A) → B) x_1) ⋯ :
        ↥(FixedPoints.subsemiring B G))

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inst_5 : FaithfulSMul A B
hA : IsGaloisGroup G A B
x : ↥(FixedPoints.subsemiring B G)
⊢ (algebraMap A B : (a : A) → B)
      ((RingEquiv.symm (ringEquivFixedPoints G A B) : (a : ↥(FixedPoints.subsemiring B G)) → A) x : A) =
    (↑x : B)

Tactic:
(hA.isInvariant.isInvariant x x.prop).choose_spec

Premises used: Exists.choose_spec, Algebra.IsInvariant.isInvariant, Subtype.prop, Classical.choose, Subtype.val
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inst_6 : CommSemiring A'
inst_7 : Algebra A' B
inst_8 : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A
⊢ Eq.{u_4 + 1} (α := B) ((algebraMap A' B : (a : A') → B) ((ringEquiv G A A' B : (a : A) → A') x : A') : B)
    ((algebraMap A B : (a : A) → B) x : B)

Tactic:
simp [ringEquiv]

Premises used: IsGaloisGroup.ringEquiv
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inst_6 : CommSemiring A'
inst_7 : Algebra A' B
inst_8 : FaithfulSMul A' B
hA' : IsGaloisGroup G A' B
x : A'
⊢ Eq.{u_4 + 1} (α := B)
    ((algebraMap A B : (a : A) → B) ((RingEquiv.symm (ringEquiv G A A' B) : (a : A') → A) x : A) : B)
    ((algebraMap A' B : (a : A') → B) x : B)

Tactic:
simp [ringEquiv]

Premises used: IsGaloisGroup.ringEquiv
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
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:
simp_rw [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ ∀ (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]
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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

Tactic:
⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩

Premises used: IsFractionRing.injective, Algebra.IsInvariant.mk, IsGaloisGroup.mk, FaithfulSMul.mk, SMulCommClass.mk
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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)
refine_3 : ∀ (x : B) (h : ∀ (g : G), g • x = x), ∃ (a : A), (algebraMap A B : (a : A) → B) a = x
⊢ IsGaloisGroup G A B

Tactic:
refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ FaithfulSMul G L

Tactic:
have := hGKL.faithful
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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₂

Tactic:
eq_of_smul_eq_smul fun (y : L) ↦ ?_

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
refine_1 : ∀ (y : L), m₁ • y = m₂ • y
⊢ m₁ = m₂

Tactic:
refine eq_of_smul_eq_smul fun (y : L) ↦ ?_

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
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)
⊢ m₁ • y = m₂ • y

Tactic:
obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective B y

Premises used: IsFractionRing.div_surjective, rfl