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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : IsFractionRing.{u_1, u_4} (A ⧸ P) K
inst_19 : IsFractionRing.{u_2, u_5} (B ⧸ Q) L
x : MulSemiringAction.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L :=
  MulSemiringAction.compHom (M := Gal(L/K)) L (stabilizerHom G P Q K L)
f : Gal(L/K)
g : ↥(MulAction.stabilizer G Q)
hg :
  Eq.{u_5 + 1} (α := Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
    ((MulSemiringAction.toAlgAut (↥(MulAction.stabilizer G Q))
            (↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)) L :
          (a : ↥(MulAction.stabilizer G Q)) → Gal(L/↥(FixedPoints.subfield (↥(MulAction.stabilizer G Q)) L)))
        g :
      Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
    (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ :
      Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hg :
      ∀ (a : L),
        Eq (α := L)
          ((((MulSemiringAction.toAlgAut (↥(MulAction.stabilizer G Q))
                        (↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)) L :
                      (a : ↥(MulAction.stabilizer G Q)) →
                        Gal(L/↥(FixedPoints.subfield (↥(MulAction.stabilizer G Q)) L)))
                    g :
                  Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L))) :
                (a : L) → L)
              a :
            L)
          ((AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ : (a : L) → L) a : L))
    (a : L),
    Eq (α := L)
      (((((stabilizerHom G P Q K L : MonoidHom.{u_3, u_5} ↥(MulAction.stabilizer G Q) Gal(L/K)) :
                  (a : ↥(MulAction.stabilizer G Q)) → Gal(L/K))
                g :
              Gal(L/K)) :
            (a : L) → L)
          a :
        L)
      ((f : (a : L) → L) a : L)
⊢ ((stabilizerHom G P Q K L : MonoidHom.{u_3, u_5} ↥(MulAction.stabilizer G Q) Gal(L/K)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal(L/K))
      g =
    f

Tactic:
rwa [AlgEquiv.ext_iff] at hg ⊢

Premises used: AlgEquiv.ext_iff
-- 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
K : Type u_4
L : Type u_5
inst_9 : Field K
inst_10 : Field L
inst_11 : Algebra.{u_1, u_4} (A ⧸ P) K
inst_12 : Algebra.{u_2, u_5} (B ⧸ Q) L
inst_13 : Algebra.{u_1, u_5} (A ⧸ P) L
inst_14 : IsScalarTower.{u_1, u_2, u_5} (A ⧸ P) (B ⧸ Q) L
inst_15 : Algebra K L
inst_16 : IsScalarTower.{u_1, u_4, u_5} (A ⧸ P) K L
inst_17 : Algebra.IsInvariant A B G
inst_18 : IsFractionRing.{u_1, u_4} (A ⧸ P) K
inst_19 : IsFractionRing.{u_2, u_5} (B ⧸ Q) L
x : MulSemiringAction.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L :=
  MulSemiringAction.compHom (M := Gal(L/K)) L (stabilizerHom G P Q K L)
f : Gal(L/K)
g : ↥(MulAction.stabilizer G Q)
hg :
  Eq.{u_5 + 1} (α := Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
    ((MulSemiringAction.toAlgAut (↥(MulAction.stabilizer G Q))
            (↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)) L :
          (a : ↥(MulAction.stabilizer G Q)) → Gal(L/↥(FixedPoints.subfield (↥(MulAction.stabilizer G Q)) L)))
        g :
      Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
    (AlgEquiv.ofRingEquiv (f := f.toRingEquiv) ⋯ :
      Gal(L/↥(FixedPoints.subfield.{u_3, u_5} (↥(MulAction.stabilizer G Q)) L)))
⊢ ∃ (a : ↥(MulAction.stabilizer G Q)),
    ((stabilizerHom G P Q K L : MonoidHom.{u_3, u_5} ↥(MulAction.stabilizer G Q) Gal(L/K)) :
          (a : ↥(MulAction.stabilizer G Q)) → Gal(L/K))
        a =
      f

Tactic:
exact ⟨g, by rwa [AlgEquiv.ext_iff] at hg ⊢⟩
-- 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
⊢ P.IsPrime

Tactic:
have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
this : P.IsPrime
x : Algebra.{u_1, u_2} (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :=
  FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
    (⇑(IsFractionRing.stabilizerHom G P Q (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :
          MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P))) :
      (a : ↥(MulAction.stabilizer G Q)) → Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))

Tactic:
have key := IsFractionRing.stabilizerHom_surjective G P Q
    (FractionRing (A ⧸ P)) (FractionRing (B ⧸ 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
this : P.IsPrime
x : Algebra.{u_1, u_2} (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :=
  FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key :
  Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
    (⇑(IsFractionRing.stabilizerHom G P Q (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :
          MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P))) :
      (a : ↥(MulAction.stabilizer G Q)) → Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
    (Function.comp (β := AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
      (⇑(IsFractionRing.fieldEquivOfAlgEquivHom.{u_1, u_2, u_1, u_2} (A := A ⧸ P) (B := B ⧸ Q) (FractionRing (A ⧸ P))
              (FractionRing (B ⧸ Q)) :
            AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q) →* Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P))) :
        (a : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) → Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
      (⇑(stabilizerHom Q P G) : (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q))

Tactic:
rw [IsFractionRing.stabilizerHom, MonoidHom.coe_comp] at key

Premises used: MonoidHom.coe_comp, IsFractionRing.stabilizerHom
-- 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
this : P.IsPrime
x : Algebra.{u_1, u_2} (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :=
  FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key :
  Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
    (Function.comp (β := AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
      (⇑(IsFractionRing.fieldEquivOfAlgEquivHom.{u_1, u_2, u_1, u_2} (A := A ⧸ P) (B := B ⧸ Q) (FractionRing (A ⧸ P))
              (FractionRing (B ⧸ Q)) :
            AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q) →* Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P))) :
        (a : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) → Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
      (⇑(stabilizerHom Q P G) : (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
    (⇑(stabilizerHom Q P G) : (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)

Tactic:
key.of_comp_left (IsFractionRing.fieldEquivOfAlgEquivHom_injective (A ⧸ P) (B ⧸ Q)
    (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))

Premises used: FractionRing, Function.Surjective.of_comp_left, HasQuotient.Quotient, IsFractionRing.fieldEquivOfAlgEquivHom_injective
-- 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
this : P.IsPrime
x : Algebra.{u_1, u_2} (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) :=
  FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key :
  Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
    (Function.comp (β := AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
      (⇑(IsFractionRing.fieldEquivOfAlgEquivHom.{u_1, u_2, u_1, u_2} (A := A ⧸ P) (B := B ⧸ Q) (FractionRing (A ⧸ P))
              (FractionRing (B ⧸ Q)) :
            AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q) →* Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P))) :
        (a : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) → Gal(FractionRing (B ⧸ Q)/FractionRing (A ⧸ P)))
      (⇑(stabilizerHom Q P G) : (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q))
⊢ Function.Surjective.{u_3 + 1, u_2 + 1} (α := ↥(MulAction.stabilizer G Q)) (β :=
    AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
    (⇑(stabilizerHom Q P G) : (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)

Tactic:
exact key.of_comp_left (IsFractionRing.fieldEquivOfAlgEquivHom_injective (A ⧸ P) (B ⧸ Q)
    (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))

Premises used: FractionRing, Function.Surjective.of_comp_left, HasQuotient.Quotient, IsFractionRing.fieldEquivOfAlgEquivHom_injective
-- 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_3
inst_3 : Group G
inst_4 : Finite G
inst_5 : MulSemiringAction G B
inst_6 : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst_7 : Q.IsPrime
inst_8 : Q.LiesOver P
inst_9 : Algebra.IsInvariant A B G
g : ↥(MulAction.stabilizer G Q)
⊢ Eq.{u_2 + 1} (α := AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
    (((stabilizerQuotientInertiaEquiv G P Q :
            MulEquiv.{u_3, u_2}
              (HasQuotient.Quotient ↥(MulAction.stabilizer G Q) (B := Subgroup ↥(MulAction.stabilizer G Q))
                (Subgroup.subgroupOf (inertia G Q) (MulAction.stabilizer G Q)))
              (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
          (a : ↥(MulAction.stabilizer G Q) ⧸ (inertia G Q).subgroupOf (MulAction.stabilizer G Q)) →
            (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
        (↑g : ↥(MulAction.stabilizer G Q) ⧸ (inertia G Q).subgroupOf (MulAction.stabilizer G Q)) :
      AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))
    (((stabilizerHom Q P G :
            MonoidHom.{u_3, u_2} (↥(MulAction.stabilizer G Q)) (AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))) :
          (a : ↥(MulAction.stabilizer G Q)) → (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q)
        g :
      AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q))

Tactic:
rfl

Premises used: Ideal.Quotient.algEquivOfEqMap, Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)

Tactic:
have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
this : (σ.comp f).range ≤ f.range
e : AlgEquiv.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) ↥f.range := AlgEquiv.ofInjective f hf
⊢ ∃ (τ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (x : B ⧸ Q),
      Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)

Tactic:
⟨(e.symm.toAlgHom.comp (Subalgebra.inclusion this)).comp (σ.comp f).rangeRestrict,
      fun x ↦ congr_arg Subtype.val (e.apply_symm_apply ⟨_, _⟩)⟩

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgHom.rangeRestrict, Subalgebra.inclusion, AlgEquiv.apply_symm_apply, Subtype.mk, congr_arg, Set.inclusion._proof_1, RingHomClass.toRingHom, Exists.intro, AlgHom.comp, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
this : (σ.comp f).range ≤ f.range
e : AlgEquiv.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) ↥f.range := AlgEquiv.ofInjective f hf
⊢ ∃ (τ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (x : B ⧸ Q),
      Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)

Tactic:
exact ⟨(e.symm.toAlgHom.comp (Subalgebra.inclusion this)).comp (σ.comp f).rangeRestrict,
      fun x ↦ congr_arg Subtype.val (e.apply_symm_apply ⟨_, _⟩)⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
suffices : (σ.comp f).range ≤ f.range
⊢ ∃ (τ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)),
    ∀ (x : B ⧸ Q),
      Eq.{u_3 + 1} (α := k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ : (a : B ⧸ Q) → B ⧸ Q) x : B ⧸ Q) : k)
        ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)

Tactic:
suffices (σ.comp f).range ≤ f.range by
    let e := (AlgEquiv.ofInjective f hf)
    exact ⟨(e.symm.toAlgHom.comp (Subalgebra.inclusion this)).comp (σ.comp f).rangeRestrict,
      fun x ↦ congr_arg Subtype.val (e.apply_symm_apply ⟨_, _⟩)⟩
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B ⧸ Q
obtain :
  ∀ (x : B),
    Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) x : k)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
intro :
  ∀ (val : Fintype G),
    Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P) k) (algebraMap A (A ⧸ P)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
⊢ IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k

Tactic:
haveI : IsScalarTower A (B ⧸ Q) k := .of_algebraMap_eq fun x ↦
    (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P) k) (algebraMap A (A ⧸ P)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
⊢ IsScalarTower A B k

Tactic:
haveI : IsScalarTower A B k := .of_algebraMap_eq fun x ↦
    (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
A : Type u_1
B : Type u_2
k : Type u_3
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 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k
inst_12 : IsDomain k
inst_13 : FaithfulSMul.{u_2, u_3} (B ⧸ Q) k
σ : AlgHom.{u_1, u_3, u_3} (A ⧸ P) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := B ⧸ Q) (β := k) (⇑f : (a : B ⧸ Q) → k)
x : B
val : Fintype G
algInst : Algebra A k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (A ⧸ P) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P) k) (algebraMap A (A ⧸ P)))
algInst_1 : Algebra B k :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ Q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ Q) k) (algebraMap B (B ⧸ Q)))
scalarTowerInst : IsScalarTower A (A ⧸ P) k := ⋯
scalarTowerInst_1 : IsScalarTower B (B ⧸ Q) k := ⋯
this_1 : IsScalarTower.{u_1, u_2, u_3} A (B ⧸ Q) k
this : IsScalarTower A B k
intro :
  ∀ (P_1 : Polynomial A)
    (hp :
      Eq.{u_2 + 1} (α := Polynomial B)
        (((Polynomial.mapRingHom (algebraMap A B) : RingHom.{u_1, u_2} (Polynomial A) (Polynomial B)) :
              (a : Polynomial A) → Polynomial B)
            P_1 :
          Polynomial B)
        (MulSemiringAction.charpoly G x : Polynomial B)),
    Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
obtain ⟨P, hp⟩ := Algebra.IsInvariant.charpoly_mem_lifts A B G x

Premises used: Algebra.IsInvariant.charpoly_mem_lifts