awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y b : B ⧸ Q
a : A ⧸ P
ha : Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
hy : Ne.{u_5 + 1} (α := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) (0 : L)
h :
  HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
      ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L)
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    HDiv.hDiv (α := L) (β := L)
        (((((IsFractionRing.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)
            ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) :
          L)
        ((algebraMap K L : (a : K) → L) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
        ((algebraMap K L : (a : K) → L) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) : L)
⊢ HDiv.hDiv (α := L) (β := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
      ((algebraMap K L : (a : K) → L) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
      ((algebraMap K L : (a : K) → L) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) : L)
have simp : ∀
  (hx :
    ∀ (g : ↥(MulAction.stabilizer G Q)),
      Eq.{u_5 + 1} (α := L)
        (((((IsFractionRing.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)
            ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) :
          L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)),
  Eq (α := L) ((f : (a : L) → L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L) : L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) b : L)
Tactic: simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
⊢ ∃ (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
have obtain : ∀ (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) sorry :
        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: obtain ⟨g, hg⟩ := FixedPoints.toAlgAut_surjective (MulAction.stabilizer G Q) L
    (AlgEquiv.ofRingEquiv (f := f) (fun x ↦ fixed_of_fixed2 G P Q K L f x x.2))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)))
⊢ ((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
have 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) sorry : (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)
Tactic: rwa [AlgEquiv.ext_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
⊢ 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)
have this : P.IsPrime
Tactic: have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)) (β :=
    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)
have 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)))
Tactic: have key := IsFractionRing.stabilizerHom_surjective G P Q
    (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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)) (β :=
    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)
have 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))
Tactic: rw [IsFractionRing.stabilizerHom, MonoidHom.coe_comp] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
⊢ ∃ (τ : 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)
have hf : 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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
⊢ ∃ (τ : 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)
have suffices : (σ.comp f).range ≤ f.range
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 ⟨_, _⟩)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) x : k)
have 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)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have 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)
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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 := ⋯
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have this : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (hypothesis)
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
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have this₁ : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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
⊢ Membership.mem (α := k) f.range (((σ.comp f).toRingHom : (a : B ⧸ Q) → k) ((mk Q : (a : B) → B ⧸ Q) x : B ⧸ Q) : k)
have 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)
Tactic: obtain ⟨P, hp⟩ := Algebra.IsInvariant.charpoly_mem_lifts A B G x
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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_1 : Ideal A
Q : Ideal B
inst_7 : Q.LiesOver P_1
inst_8 : CommRing k
inst_9 : Algebra.{u_1, u_3} (A ⧸ P_1) k
inst_10 : Algebra.{u_2, u_3} (B ⧸ Q) k
inst_11 : IsScalarTower.{u_1, u_2, u_3} (A ⧸ P_1) (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_1) k k
f : AlgHom.{u_1, u_2, u_3} (A ⧸ P_1) (B ⧸ Q) k := IsScalarTower.toAlgHom (A ⧸ P_1) (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_1) _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ P_1) k) (algebraMap A (A ⧸ P_1)))
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_1) 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
P : 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 :
      Polynomial B)
    (MulSemiringAction.charpoly G x : Polynomial B)
⊢ Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : Polynomial A) → B) P : B) (0 : B)
have rw : Polynomial.eval₂ (algebraMap A B) x P = 0
Tactic: rw [Polynomial.aeval_def, ← Polynomial.eval_map,
      ← Polynomial.coe_mapRingHom (R := A), hp, MulSemiringAction.eval_charpoly]