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
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)
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)
rwa₂ : ¬Eq.{u_4 + 1} (α := K) ((algebraMap (A ⧸ P) K : (a : A ⧸ P) → K) a : K) (0 : K)
rwa₃ rwa₄ rwa₅ rwa₆ : ¬a = 0
⊢ Ne.{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]

Premises used: Ne, HasQuotient.Quotient, IsScalarTower.algebraMap_apply, FaithfulSMul.algebraMap_eq_zero_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
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)

Tactic:
replace ha : algebraMap (A ⧸ P) L a ≠ 0 := by
    rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_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
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
h : a • x = y * b
ha : Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) (0 : L)

Tactic:
replace hy : algebraMap (B ⧸ Q) L y ≠ 0 :=
    mt (algebraMap_eq_zero_iff (B ⧸ Q) L).mp (nonZeroDivisors.ne_zero hy)
-- 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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
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
h : a • x = y * b
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)
⊢ HMul.hMul (β := B ⧸ Q) x ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q) = b * y

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

Premises used: mul_comm, Algebra.smul_def
-- 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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
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
h : a • x = y * b
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₁ : HMul.hMul (β := B ⧸ Q) x ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q) = b * y
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)

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

Premises used: mul_comm, Algebra.smul_def
-- 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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
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
h : a • x = y * b
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₁ : HMul.hMul (β := B ⧸ Q) x ((algebraMap (A ⧸ P) (B ⧸ Q) : (a : A ⧸ P) → B ⧸ Q) a : B ⧸ Q) = b * y
ha₁ : Ne.{u_5 + 1} (α := L) ((algebraMap (A ⧸ P) L : (a : A ⧸ P) → L) a : L) (0 : L)
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap (B ⧸ Q) L : (a : B ⧸ Q) → L) y : L) (0 : L)

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

Premises used: mul_comm, Algebra.smul_def
-- 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
f : Gal(L/K)
val : Fintype G
this_1 : P.IsPrime
this : Algebra.IsIntegral A B
x y : B ⧸ Q
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
h : a • x = y * b
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)
⊢ 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)

Tactic:
replace h : algebraMap (B ⧸ Q) L x / algebraMap (B ⧸ Q) L y =
      algebraMap (B ⧸ Q) L b / algebraMap (A ⧸ P) L a := by
    rw [mul_comm, Algebra.smul_def, mul_comm] at h
    rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← 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_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)
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)
⊢ 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)

Tactic:
simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢

Premises used: div_left_inj', IsScalarTower.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_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)),
    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:
fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
    ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
      (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

Premises used: _private.0.fixed_of_fixed1, IsFractionRing.injective, IsFractionRing.fieldEquivOfAlgEquiv_algebraMap, HasQuotient.Quotient, Eq.symm, DFunLike.coe, Ideal.Quotient.stabilizerHom, Eq.trans
-- 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
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)),
    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:
exact fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
    ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
      (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

Premises used: _private.0.fixed_of_fixed1, IsFractionRing.injective, IsFractionRing.fieldEquivOfAlgEquiv_algebraMap, HasQuotient.Quotient, Eq.symm, DFunLike.coe, Ideal.Quotient.stabilizerHom, Eq.trans
-- 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)
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) ⋯ :
          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
⊢ ∃ (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))

Premises used: Membership.mem, Subtype, FixedPoints.toAlgAut_surjective, AlgEquiv.ofRingEquiv, MulAction.stabilizer, Subtype.val, _private.0.fixed_of_fixed2, Subtype.property