awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x : B
refine_2 :
  ∀ (y : B)
    (e :
      Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q)
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)),
    (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
        ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
      (mk Q : (a : B) → B ⧸ Q) x
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x

Tactic:
obtain ⟨y, e⟩ := Ideal.Quotient.mk_surjective (τ₂ (Ideal.Quotient.mk Q x))

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, 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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((f : (a : B ⧸ Q) → k)
        ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
          ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x))) :
      k)
    ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ (↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
      ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) =
    (mk Q : (a : B) → B ⧸ Q) x

Tactic:
apply hf
-- 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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
      (((↑σ : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      (((↑σ.symm : k →ₐ[A ⧸ P] k) : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
⊢ Eq.{u_3 + 1} (α := k)
    ((f : (a : B ⧸ Q) → k)
        ((↑(↑τ₁.toRingHom : B ⧸ Q →* B ⧸ Q) : OneHom (B ⧸ Q) (B ⧸ Q)).toFun
          ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x))) :
      k)
    ((f : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
dsimp [f] at h₁ h₂ ⊢
-- 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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
.trans ?_ (σ.apply_symm_apply _)

Premises used: AlgEquiv.apply_symm_apply, Eq.trans
-- 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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) :
          k) :
      k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)

Tactic:
refine .trans ?_ (σ.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
σ : AlgEquiv.{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)
τ₁ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₁ :
  ∀ (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)
τ₂ : AlgHom.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
h₂ :
  ∀ (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)
      ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) x : k) : k)
x y : B
e :
  Eq (α := B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q)
refine_2 :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x) : B ⧸ Q) :
          k) :
      k)
refine_2₁ :
  Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) y) : B ⧸ Q) : k)
    ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
refine_2₂ refine_2₃ :
  Eq (α := k)
    ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
    ((σ : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) y : B ⧸ Q) : k) : k)
⊢ Eq.{u_3 + 1} (α := k)
    ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k)
        ((τ₁ : (a : B ⧸ Q) → B ⧸ Q) ((τ₂ : (a : B ⧸ Q) → B ⧸ Q) ((mk Q : (a : B) → B ⧸ Q) x)) : B ⧸ Q) :
      k)
    ((σ : (a : k) → k)
        ((σ.symm : (a : k) → k) ((algebraMap (B ⧸ Q) k : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k) :
          k) :
      k)

Tactic:
rw [← h₂, ← e, h₁]
-- 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
inl : Subsingleton B → Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
inr : Nontrivial B → Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
cases subsingleton_or_nontrivial B

Premises used: subsingleton_or_nontrivial
-- 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 : Subsingleton B
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
cases ‹Q.IsMaximal›.ne_top (Subsingleton.elim _ _)

Premises used: Ideal.IsMaximal.ne_top, Subsingleton.elim
-- 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
⊢ Algebra.IsIntegral A B

Tactic:
have := Algebra.IsInvariant.isIntegral A B G
-- 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 : Algebra.IsIntegral A B
inr :
  ∀ (x : B ⧸ Q),
    Polynomial.Splits.{u_2} (R := B ⧸ Q)
      (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (minpoly (A ⧸ P) x))
⊢ Normal.{u_1, u_2} (A ⧸ P) (B ⧸ Q)

Tactic:
constructor
-- 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 : Algebra.IsIntegral A B
x : B ⧸ Q
inr :
  ∀ (x : B),
    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)))
⊢ Polynomial.Splits.{u_2} (R := B ⧸ Q)
    (Polynomial.map.{u_1, u_2} (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (minpoly (A ⧸ P) x))

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
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 : Algebra.IsIntegral A B
x : B
inr :
  ∀ (val : Fintype G),
    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)))
⊢ 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:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- 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 : Algebra.IsIntegral A B
x : B
val : Fintype G
inr :
  ∀ (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),
    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)))
⊢ 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:
obtain ⟨p, hp, h₁, h₂⟩ := Polynomial.lifts_and_degree_eq_and_monic
    (Algebra.IsInvariant.charpoly_mem_lifts A B G x) (MulSemiringAction.monic_charpoly _ _)

Premises used: Polynomial.lifts_and_degree_eq_and_monic, MulSemiringAction.monic_charpoly, Algebra.IsInvariant.charpoly_mem_lifts
-- 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 : 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
rw : Polynomial.eval₂ (algebraMap A B) x p = 0
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap A B) p) = 0
rw₂ : Polynomial.eval x (MulSemiringAction.charpoly G x) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := B) 0 0
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)

Tactic:
rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]

Premises used: Polynomial.eval_map, Polynomial.aeval_def, MulSemiringAction.eval_charpoly
-- 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 : 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
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) p : B) (0 : B)

Tactic:
have H : Polynomial.aeval x p = 0 := by
    rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
-- 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 : 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)
rw :
  Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} A (Polynomial A) (B ⧸ Q)) :
          (a : Polynomial A) → B ⧸ Q)
        p :
      B ⧸ Q)
    (0 : B ⧸ Q)
rw₁ :
  Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) ((Polynomial.aeval x : (a : Polynomial A) → B) p) : B ⧸ Q)
    (0 : B ⧸ Q)
rw₂ : Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) 0) 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := B ⧸ Q) 0 0
⊢ Eq.{u_2 + 1} (α := B ⧸ Q)
    (((Polynomial.aeval ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) x) :
            AlgHom.{u_1, u_1, u_2} (A ⧸ P) (Polynomial (A ⧸ P)) (B ⧸ Q)) :
          (a : Polynomial (A ⧸ P)) → B ⧸ Q)
        (Polynomial.map (algebraMap A (A ⧸ P)) p) :
      B ⧸ Q)
    (0 : B ⧸ Q)

Tactic:
rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero]

Premises used: Polynomial.aeval_map_algebraMap, map_zero, Polynomial.aeval_algebraMap_apply
-- 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 : 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)
⊢ 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)

Tactic:
have := minpoly.dvd _ (algebraMap _ (B ⧸ Q) x) (p := p.map (algebraMap _ (A ⧸ P)))
    (by rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_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)
⊢ 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:
Polynomial.Splits.of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)

Premises used: Iff.mpr, Polynomial.Splits.of_dvd, Polynomial.map_dvd_map'