awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
inr :
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p))
inr₁ :
  Ne.{u_2 + 1} (α := Polynomial (B ⧸ Q))
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p)) 0
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q))
      (minpoly (A ⧸ P) (B := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q)))

Tactic:
refine Polynomial.Splits.of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)

Premises used: Iff.mpr, Polynomial.Splits.of_dvd, Polynomial.map_dvd_map'
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
inr :
  Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (∏ i : G,
      Polynomial.map (algebraMap B (B ⧸ Q))
        (HSub.hSub (α := Polynomial B) (β := Polynomial B) Polynomial.X
          ((Polynomial.C : (a : B) → Polynomial B) (i • x) : Polynomial B)))
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p))

Tactic:
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B,
      ← Polynomial.map_map, hp, MulSemiringAction.charpoly_eq, Polynomial.map_prod]

Premises used: Polynomial.map_prod, MulSemiringAction.charpoly_eq, IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (∏ i : G,
      Polynomial.map (algebraMap B (B ⧸ Q))
        (HSub.hSub (α := Polynomial B) (β := Polynomial B) Polynomial.X
          ((Polynomial.C : (a : B) → Polynomial B) (i • x) : Polynomial B)))

Tactic:
Polynomial.Splits.prod (fun _ _ ↦ (Polynomial.Splits.X_sub_C _).map _)

Premises used: Algebra.algebraMap, HasQuotient.Quotient, Polynomial.Splits.X_sub_C, HSMul.hSMul, Polynomial.Splits.map, Polynomial.Splits.prod
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (∏ i : G,
      Polynomial.map (algebraMap B (B ⧸ Q))
        (HSub.hSub (α := Polynomial B) (β := Polynomial B) Polynomial.X
          ((Polynomial.C : (a : B) → Polynomial B) (i • x) : Polynomial B)))

Tactic:
exact Polynomial.Splits.prod (fun _ _ ↦ (Polynomial.Splits.X_sub_C _).map _)

Premises used: Polynomial.Splits.X_sub_C, Polynomial.Splits.map, Polynomial.Splits.prod
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Ne.{u_2 + 1} (α := Polynomial (B ⧸ Q))
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p)) 0

Tactic:
((h₂.map _).map _).ne_zero

Premises used: Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
h : Nontrivial B
this_1 : Algebra.IsIntegral A B
x : B
val : Fintype G
p : Polynomial A
hp : Eq (α := Polynomial B) (Polynomial.map (algebraMap A B) p) (MulSemiringAction.charpoly G x)
h₁ : p.degree = Polynomial.degree (MulSemiringAction.charpoly G x)
h₂ : p.Monic
H : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)
this :
  Dvd.dvd (α := Polynomial (A ⧸ P)) (minpoly (A ⧸ P) (B := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x : B ⧸ Q))
    (Polynomial.map (algebraMap A (A ⧸ P)) p)
⊢ Ne.{u_2 + 1} (α := Polynomial (B ⧸ Q))
    (Polynomial.map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (Polynomial.map (algebraMap A (A ⧸ P)) p)) 0

Tactic:
exact ((h₂.map _).map _).ne_zero

Premises used: Polynomial.Monic.map, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
have : IsGalois (A ⧸ P) (B ⧸ Q) := { __ := Ideal.Quotient.normal (A := A) G P Q }
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this : IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ Finite.{u_2 + 1} Gal((B ⧸ Q)/A ⧸ P)

Tactic:
have := Finite.of_surjective _ (Ideal.Quotient.stabilizerHom_surjective G P Q)
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this_1 : IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this : Finite.{u_2 + 1} Gal((B ⧸ Q)/A ⧸ P)
⊢ Module.Finite.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
IsGalois.finiteDimensional_of_finite _ _

Premises used: IsGalois.finiteDimensional_of_finite
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u_4
inst_3 : Finite G
inst_4 : Group G
inst_5 : MulSemiringAction G B
inst_6 : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P
inst_8 : P.IsMaximal
inst_9 : Q.IsMaximal
inst_10 : SMulCommClass G A B
inst_11 : Algebra.IsSeparable.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this_1 : IsGalois.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
this : Finite.{u_2 + 1} Gal((B ⧸ Q)/A ⧸ P)
⊢ Module.Finite.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
exact IsGalois.finiteDimensional_of_finite _ _

Premises used: IsGalois.finiteDimensional_of_finite
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
⊢ Algebra.IsInvariant K L G

Tactic:
⟨fun x h ↦ ?_⟩

Premises used: Algebra.IsInvariant.mk
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
refine : ∀ (x : L) (h : ∀ (g : G), g • x = x), ∃ (a : K), (algebraMap K L : (a : K) → L) a = x
⊢ Algebra.IsInvariant K L G

Tactic:
refine ⟨fun x h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
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.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
⊢ ∀ (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.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
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)
⊢ Algebra.IsIntegral A B

Tactic:
have := hAB.isIntegral A B G
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
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)
this : Algebra.IsIntegral A B
⊢ Nontrivial A

Tactic:
have : Nontrivial A := (IsFractionRing.nontrivial_iff_nontrivial A K).mpr inferInstance
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
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)
this_1 : Algebra.IsIntegral A B
this : Nontrivial A
⊢ Nontrivial B

Tactic:
have : Nontrivial B := (IsFractionRing.nontrivial_iff_nontrivial B L).mpr inferInstance
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
x : L
h : ∀ (g : G), g • x = x
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)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
obtain :
  ∀ (x y : B) (hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y)
    (h :
      ∀ (g : G),
        g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
          HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)),
    ∃ (a : K),
      (algebraMap K L : (a : K) → L) a =
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ ∃ (a : K), (algebraMap K L : (a : K) → L) a = x

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G 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)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)

Tactic:
simpa using nonZeroDivisors.ne_zero hy

Premises used: nonZeroDivisors.ne_zero
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G 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)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)

Tactic:
have hy' : algebraMap B L y ≠ 0 := by simpa using nonZeroDivisors.ne_zero hy
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G 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)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
obtain :
  ∀ (b : B) (a : A) (ha : a ≠ 0) (hb : a • x = y * b),
    ∃ (a : K),
      (algebraMap K L : (a : K) → L) a =
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)

Tactic:
obtain ⟨b, a, ha, hb⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A) y).exists_smul_eq_mul x hy

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.exists_smul_eq_mul
-- Module: Mathlib.RingTheory.Invariant.Basic
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
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G 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)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
ha : a ≠ 0
hb : a • x = y * b
⊢ HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y

Tactic:
rw [mul_comm, Algebra.smul_def, mul_comm] at hb

Premises used: mul_comm, Algebra.smul_def