awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.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)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₀ : ∀ (g : G),
  map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
    if g • Q = Q then
      HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
    else X
Tactic: have key₀ : ∀ g : G, (X - C (g • b)).map (algebraMap B (B ⧸ Q)) =
      if g • Q = Q then X - C (algebraMap B (B ⧸ Q) (a * b₀)) else X := by
    intro g
    rw [Polynomial.map_sub, map_X, map_C, hb]
    split_ifs
    · rfl
    · rw [map_zero, map_zero, sub_zero]
-- 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
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 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.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)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key :
  Eq.{u_2 + 1} (α := (B ⧸ Q)[X]) (map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M))
    (∏ i : G, map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (i • b) : B[X])))
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
      if g • Q = Q then
        HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
          ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
      else X
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₁ : map (R := A ⧸ P) (algebraMap (A ⧸ P) (B ⧸ Q)) (map (algebraMap A (A ⧸ P)) M) =
  HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
        ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X]) ^
      Finset.card.{u_3} (α := G) {x : G | x • Q = Q} *
    HPow.hPow (α := (B ⧸ Q)[X]) X (Finset.card.{u_3} (α := G) {x : G | ¬x • Q = Q})
Tactic: simp only [key₀, Finset.prod_ite, Finset.prod_const] at key
Cleared hypotheses: key
-- 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
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 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.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)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
      if g • Q = Q then
        HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
          ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
      else X
key :
  map (algebraMap K L) (map (R := A ⧸ P) (algebraMap (A ⧸ P) K) (map (algebraMap A (A ⧸ P)) M)) =
    HSub.hSub (α := L[X]) (β := L[X]) X
          ((C : (a : L) → L[X])
              ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q)) :
            L[X]) ^
        Finset.card.{u_3} (α := G) {x : G | x • Q = Q} *
      HPow.hPow (α := L[X]) X (Finset.card.{u_3} (α := G) {x : G | ¬x • Q = Q})
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₁ : Eq (α := L)
  ((f : (a : L) → L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L) :
    L)
  ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L)
Tactic: replace key := fixed_of_fixed1_aux3 key f (Finset.card_ne_zero_of_mem
    (Finset.mem_filter.mpr ⟨Finset.mem_univ 1, one_smul G Q⟩))
Cleared hypotheses: key
-- 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
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 : Module.IsTorsionFree.{u_2, u_5} (B ⧸ Q) L
f : Gal(L/K)
val : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    Eq (α := B ⧸ Q)
      (((((Ideal.Quotient.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)) :
            (a : B ⧸ Q) → B ⧸ Q)
          ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀) :
        B ⧸ Q)
      ((Ideal.Quotient.mk Q : (a : B) → B ⧸ Q) b₀ : B ⧸ Q)
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb :
  ∀ (g : G),
    Eq (α := B ⧸ Q) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (g • b) : B ⧸ Q)
      ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (if g • Q = Q then a * b₀ else 0) : B ⧸ Q)
M : A[X]
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (HSub.hSub (α := B[X]) (β := B[X]) X ((C : (a : B) → B[X]) (g • b) : B[X])) =
      if g • Q = Q then
        HSub.hSub (α := (B ⧸ Q)[X]) (β := (B ⧸ Q)[X]) X
          ((C : (a : B ⧸ Q) → (B ⧸ Q)[X]) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀)) : (B ⧸ Q)[X])
      else X
key :
  Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) (a * b₀) : B ⧸ Q) : L)
⊢ Eq (α := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L)
            (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) :
          L) :
      L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) (((algebraMap B (B ⧸ Q) : B →+* B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
have key₁ : HMul.hMul (α := L) (β := L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q) : L) :
      L)
    ((f : (a : L) → L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L) :
      L) =
  HMul.hMul (α := L) (β := L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) a : B ⧸ Q) : L)
    ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) ((algebraMap B (B ⧸ Q) : (a : B) → B ⧸ Q) b₀ : B ⧸ Q) : L)
Tactic: simp only [map_mul] at key
Cleared hypotheses: key
-- 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)
x : L
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        x =
      x
⊢ (f : (a : L) → L) x = x
have obtain : ∀ (val : Fintype G), (f : (a : L) → L) x = x
Tactic: obtain ⟨_⟩ := nonempty_fintype G
-- 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
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)
x : L
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        x =
      x
val : Fintype G
⊢ (f : (a : L) → L) x = x
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
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)
x : L
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        x =
      x
val : Fintype G
this : P.IsPrime
⊢ (f : (a : L) → L) x = x
have this₁ : Algebra.IsIntegral A B
Tactic: have : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G
-- 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)
x : L
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        x =
      x
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
⊢ (f : (a : L) → L) x = x
have obtain : ∀ (x y : B ⧸ Q) (hy : Membership.mem (γ := Submonoid (B ⧸ Q)) (nonZeroDivisors (B ⧸ Q)) y)
  (hx :
    ∀ (g : ↥(MulAction.stabilizer G Q)),
      ((((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)
          (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) x : L)
          ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)),
  (f : (a : L) → L)
      (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) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x
Cleared hypotheses: x, 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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
hy : Membership.mem (γ := Submonoid (B ⧸ Q)) (nonZeroDivisors (B ⧸ Q)) y
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        (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) x : L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
⊢ (f : (a : L) → L)
      (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) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
have obtain : ∀ (b : B ⧸ Q) (a : A ⧸ P) (ha : a ≠ 0) (h : a • x = y * b),
  (f : (a : L) → L)
      (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) x : L)
      ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
Tactic: obtain ⟨b, a, ha, h⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A ⧸ P) y).exists_smul_eq_mul x hy
-- 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 ⧸ Q
hy : Membership.mem (γ := Submonoid (B ⧸ Q)) (nonZeroDivisors (B ⧸ Q)) y
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        (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) x : L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
have rwa : ¬Eq.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
Tactic: rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]
-- 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 ⧸ Q
hy : Membership.mem (γ := Submonoid (B ⧸ Q)) (nonZeroDivisors (B ⧸ Q)) y
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((((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)
        (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) x : L)
        ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L)
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
rwa : ¬Eq.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
have rwa₁ : ¬Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) : L) (0 : L)
Tactic: rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]