awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
simp only [smul_div₀', ← algebraMap.coe_smul', h]

Premises used: algebraMap.coe_smul', smul_div₀'
-- 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)
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:
simp [Algebra.smul_def, algebraMap.coe_smul', ← hc]

Premises used: algebraMap.coe_smul', Algebra.smul_def
-- 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)
x : B
h : ∀ (g : G), g • x = x
⊢ ∀ (g : G), HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) x : L) = (algebraMap B L : (a : B) → L) x

Tactic:
simpa [← algebraMap.coe_smul']

Premises used: algebraMap.coe_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)
x : B
h : ∀ (g : G), g • x = x
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
⊢ ∃ (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'])

Premises used: Algebra.algebraMap, Algebra.IsInvariant.isInvariant, DFunLike.coe
-- 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)
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)
⊢ 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
-- 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)
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)
⊢ ∃ (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

Premises used: IsIntegrallyClosedIn.isIntegral_iff, Algebra.algebraMap, RingHom.injective, isIntegral_algebraMap_iff
-- 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)
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
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
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x

Tactic:
obtain ⟨a, rfl⟩ := hx

Premises used: rfl
-- 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)
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hb : (algebraMap A B : (a : A) → B) a = x), (algebraMap A B : (a : A) → B) a = x
⊢ (algebraMap A B : (a : A) → B) a = x

Tactic:
rwa [hc, IsFractionRing.coe_inj] at hb

Premises used: IsFractionRing.coe_inj
-- 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)
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)
⊢ ∃ (a : A), (algebraMap A B : (a : A) → B) a = x

Tactic:
exact ⟨a, by rwa [hc, IsFractionRing.coe_inj] at hb⟩
-- 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
inst_17 : Finite G
inst_18 : IsIntegrallyClosed A
⊢ IsGaloisGroup G A B ↔ Algebra.IsIntegral A B ∧ IsGaloisGroup G K L

Tactic:
⟨fun h ↦ ⟨h.isInvariant.isIntegral, h.to_isFractionRing G A B K L⟩,
    fun ⟨_, h⟩ ↦ h.of_isFractionRing G A B K L⟩

Premises used: _private.0.IsGaloisGroup.iff_isFractionRing.match_1, IsGaloisGroup.of_isFractionRing, And.intro, Iff.intro, IsGaloisGroup.to_isFractionRing, IsGaloisGroup, Algebra.IsInvariant.isIntegral
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
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)
⊢ g • b • x = (g • b) • g • x

Tactic:
rw [Algebra.smul_def', Algebra.smul_def', smul_mul']

Premises used: Algebra.smul_def', smul_mul'
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
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)
⊢ 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:
congr
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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) =
    (algebraMap B (FractionRing B) : (a : B) → FractionRing B) (g • b)

Tactic:
IsFractionRing.fieldEquivOfAlgEquiv_algebraMap (FractionRing A) _ _ _ b

Premises used: FractionRing, IsFractionRing.fieldEquivOfAlgEquiv_algebraMap, SMul.comp.smul
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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) =
    (algebraMap B (FractionRing B) : (a : B) → FractionRing B) (g • b)

Tactic:
exact IsFractionRing.fieldEquivOfAlgEquiv_algebraMap (FractionRing A) _ _ _ b

Premises used: FractionRing, IsFractionRing.fieldEquivOfAlgEquiv_algebraMap
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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)
⊢ 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⟩
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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_1 : MulSemiringAction.{u_1, u_3} G (FractionRing B) :=
  IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
this : SMulDistribClass G B (FractionRing B)
⊢ IsGaloisGroup.{u_1, u_2, u_3} G (FractionRing A) (FractionRing B)

Tactic:
apply IsGaloisGroup.to_isFractionRing G A B _ _

Premises used: IsGaloisGroup.to_isFractionRing
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G_1 : Type u_1
A : Type u_2
B : Type u_3
K_1 : Type u_4
L_1 : Type u_5
inst : Group G_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G_1 B
inst_4 : Algebra A B
inst_5 : Field K_1
inst_6 : Field L_1
inst_7 : Algebra K_1 L_1
inst_8 : Algebra A K_1
inst_9 : Algebra B L_1
inst_10 : Algebra A L_1
inst_11 : IsFractionRing A K_1
inst_12 : IsFractionRing B L_1
inst_13 : IsScalarTower A K_1 L_1
inst_14 : IsScalarTower A B L_1
inst_15 : MulSemiringAction G_1 L_1
inst_16 : SMulDistribClass G_1 B L_1
K : Type u_6
L : Type u_7
inst_17 : Field K
inst_18 : Field L
inst_19 : NumberField K
inst_20 : NumberField L
inst_21 : Algebra K L
G : Type u_8
inst_22 : Group G
inst_23 : MulSemiringAction G L
inst_24 : IsGaloisGroup G K L
⊢ IsGaloisGroup.{u_8, u_6, u_7} G (𝓞 K) (𝓞 L)

Tactic:
IsGaloisGroup.of_isFractionRing G (𝓞 K) (𝓞 L) K L

Premises used: IsGaloisGroup.of_isFractionRing, NumberField.RingOfIntegers
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
Goal:
G_1 : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L_1 : Type u_5
inst : Group G_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G_1 B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L_1
inst_7 : Algebra K L_1
inst_8 : Algebra A K
inst_9 : Algebra B L_1
inst_10 : Algebra A L_1
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L_1
inst_13 : IsScalarTower A K L_1
inst_14 : IsScalarTower A B L_1
inst_15 : MulSemiringAction G_1 L_1
inst_16 : SMulDistribClass G_1 B L_1
L : Type u_6
inst_17 : Field L
inst_18 : NumberField L
G : Type u_7
inst_19 : Group G
inst_20 : MulSemiringAction G L
inst_21 : IsGaloisGroup G ℚ L
⊢ IsGaloisGroup.{u_7, 0, u_6} G ℤ (𝓞 L)

Tactic:
IsGaloisGroup.of_isFractionRing G ℤ (𝓞 L) ℚ L

Premises used: Rat, Int, IsGaloisGroup.of_isFractionRing, NumberField.RingOfIntegers
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
rw : LE.le.{u_4} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ LE.le.{u_4} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥

Tactic:
Algebra.IsInvariant.isInvariant

Premises used: Set.Mem, setOf, Algebra.IsInvariant.isInvariant, Set.range, MulAction.fixedPoints
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ LE.le.{u_4} (α := IntermediateField K L) (FixedPoints.intermediateField G) ⊥

Tactic:
exact Algebra.IsInvariant.isInvariant

Premises used: Algebra.IsInvariant.isInvariant
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
rw : IsGalois (↥(FixedPoints.intermediateField G)) L
⊢ IsGalois K L

Tactic:
rw [← isGalois_iff_isGalois_bot, ← fixedPoints_eq_bot G]

Premises used: isGalois_iff_isGalois_bot, IsGaloisGroup.fixedPoints_eq_bot
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 (↥(FixedPoints.intermediateField G)) L

Tactic:
IsGalois.of_fixed_field L G

Premises used: Subfield.subtype, FixedPoints.intermediateField, Set.Mem, Subfield.copy, FixedPoints.subfield, IsGalois.of_fixed_field
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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 (↥(FixedPoints.intermediateField G)) L

Tactic:
exact IsGalois.of_fixed_field L G

Premises used: IsGalois.of_fixed_field
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inr : ∀ (hG : Infinite G), Nat.card G = finrank K L
⊢ Nat.card G = finrank K L

Tactic:
rcases fintypeOrInfinite G with _ | hG

Premises used: fintypeOrInfinite
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ FaithfulSMul G L

Tactic:
have : FaithfulSMul G L := faithful K
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inl : Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L
⊢ Nat.card G = finrank K L

Tactic:
rw [← IntermediateField.finrank_bot', ← fixedPoints_eq_bot G, Nat.card_eq_fintype_card]

Premises used: IntermediateField.finrank_bot', Nat.card_eq_fintype_card, IsGaloisGroup.fixedPoints_eq_bot
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L

Tactic:
(FixedPoints.finrank_eq_card G L).symm

Premises used: FixedPoints.finrank_eq_card, FixedPoints.intermediateField, Set.Mem, Subfield.copy, FixedPoints.subfield, Eq.symm
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L

Tactic:
exact (FixedPoints.finrank_eq_card G L).symm

Premises used: FixedPoints.finrank_eq_card, Eq.symm
-- Module: Mathlib.FieldTheory.Galois.IsGaloisGroup
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
inr : finrank K L = 0
⊢ Nat.card G = finrank K L

Tactic:
rw [Nat.card_eq_zero_of_infinite, eq_comm]

Premises used: Nat.card_eq_zero_of_infinite, eq_comm