awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
ha : a ≠ 0
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)

Tactic:
simpa [← hc]
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
ha : a ≠ 0
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
⊢ Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)

Tactic:
replace ha : (algebraMap B L) (algebraMap A B a) ≠ 0 := by simpa [← hc]
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
rw :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₁ :
  (algebraMap B L : (a : B) → L) (HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B)) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₂ :
  (algebraMap B L : (a : B) → L) (b * y) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
rw₃ rw₄ :
  HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)

Tactic:
rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]

Premises used: div_eq_div_iff, map_mul
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
⊢ HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)

Tactic:
have hxy : algebraMap B L x / algebraMap B L y =
    algebraMap B L b / algebraMap B L (algebraMap A B a) := by
    rw [div_eq_div_iff hy' ha, ← map_mul, hb, map_mul]
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
hxy :
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
⊢ ∀ (g : G), g • b = b

Tactic:
simpa [ha, hxy, smul_div₀', ← algebraMap.coe_smul'] using h

Premises used: algebraMap.coe_smul', smul_div₀'
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
b : B
a : A
hb : HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) = b * y
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
hxy :
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) b : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
obtain :
  ∀ (b : A)
    (hb :
      HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) =
        HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) b : B) y)
    (hxy :
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
          ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)),
    ∃ (a : K),
      (algebraMap K L : (a : K) → L) a =
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)

Tactic:
obtain ⟨b, rfl⟩ := hAB.isInvariant b
    (by simpa [ha, hxy, smul_div₀', ← algebraMap.coe_smul'] using h)

Premises used: Algebra.IsInvariant.isInvariant, rfl
-- Module: Mathlib.RingTheory.Invariant.Basic
Goal:
G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : Finite G
hAB : Algebra.IsInvariant A B G
inst_18 : SMulCommClass G A B
hc :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
this_1 : Algebra.IsIntegral A B
this_2 : Nontrivial A
this : Nontrivial B
x y : B
hy : Membership.mem (γ := Submonoid B) (nonZeroDivisors B) y
h :
  ∀ (g : G),
    g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
hy' : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) y : L) (0 : L)
a : A
ha : Ne.{u_5 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L) (0 : L)
b : A
hb :
  HMul.hMul (β := B) x ((algebraMap A B : (a : A) → B) a : B) =
    HMul.hMul (α := B) ((algebraMap A B : (a : A) → B) b : B) y
hxy :
  HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) b : B) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
h₁ :
  (algebraMap K L : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) ((algebraMap A K : (a : A) → K) a : K)) =
    HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)
⊢ ∃ (a : K),
    (algebraMap K L : (a : K) → L) a =
      HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) x : L) ((algebraMap B L : (a : B) → L) y : L)

Tactic:
use algebraMap A K b / algebraMap A K a

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
isIntegral : ∀ (x : B), IsIntegral A x
⊢ Algebra.IsIntegral A B

Tactic:
constructor
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
x : B
isIntegral : ∀ (N : OpenNormalSubgroup G) (hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G x) : Set G)), IsIntegral A x
⊢ IsIntegral A x

Tactic:
obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
    (stabilizer_isOpen G x) (one_mem _)

Premises used: ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one, OneMemClass.one_mem, stabilizer_isOpen
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G x) : Set G)
⊢ IsIntegral A (A := ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
        x)
      x ⋯)

Tactic:
have := (Algebra.IsInvariant.isIntegral A (FixedPoints.subalgebra A B N.1.1) (G ⧸ N.1.1)).1
    ⟨x, fun g ↦ hN g.2⟩
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G x) : Set G)
this :
  IsIntegral A (A := ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
        x)
      x ⋯)
⊢ IsIntegral A x

Tactic:
this.map (FixedPoints.subalgebra A B N.1.1).val

Premises used: Subalgebra.val, Membership.mem, Subtype, FixedPoints.subalgebra, IsIntegral.map, OpenNormalSubgroup.toOpenSubgroup, OpenSubgroup.toSubgroup
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G x) : Set G)
this :
  IsIntegral A (A := ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
        x)
      x ⋯)
⊢ IsIntegral A x

Tactic:
exact this.map (FixedPoints.subalgebra A B N.1.1).val

Premises used: Subalgebra.val, Membership.mem, Subtype, FixedPoints.subalgebra, IsIntegral.map, OpenNormalSubgroup.toOpenSubgroup, OpenSubgroup.toSubgroup
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
P Q : Ideal B
inst_14 : P.IsPrime
inst_15 : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
B' : (G : Type u) → [inst_16 : Monoid G] → [inst_17 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
N N' : OpenNormalSubgroup G
f : N ⟶ N'
x :
  { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
    Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
      HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
        (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) }
⊢ B' ↥(↑N'.toOpenSubgroup : Subgroup G) ≤ B' ↥(↑N.toOpenSubgroup : Subgroup G)

Tactic:
have h : B' N'.1.1 ≤ B' N.1.1 := fun x hx n ↦ hx ⟨_, f.le n.2⟩
-- Module: Mathlib.RingTheory.Invariant.Profinite
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
G : Type u
inst_3 : Group G
inst_4 : MulSemiringAction G B
inst_5 : SMulCommClass G A B
inst_6 : TopologicalSpace G
inst_7 : CompactSpace G
inst_8 : TotallyDisconnectedSpace G
inst_9 : IsTopologicalGroup G
inst_10 : TopologicalSpace B
inst_11 : DiscreteTopology B
inst_12 : ContinuousSMul G B
inst_13 : IsInvariant A B G
P Q : Ideal B
inst_14 : P.IsPrime
inst_15 : Q.IsPrime
hPQ : Eq (α := Ideal A) (Ideal.under A P) (Ideal.under A Q)
B' : (G : Type u) → [inst_16 : Monoid G] → [inst_17 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
N N' : OpenNormalSubgroup G
f : N ⟶ N'
x :
  { g : G ⧸ (↑N.toOpenSubgroup : Subgroup G) //
    Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
      HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
        (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P) }
h : B' ↥(↑N'.toOpenSubgroup : Subgroup G) ≤ B' ↥(↑N.toOpenSubgroup : Subgroup G)
obtain :
  ∀ (x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
    (hx :
      Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
        HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) x
          (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P)),
    Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
      HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G)))
        ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
              (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
            (↑(Subtype.mk (p := fun (g : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) ↦
                  Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
                    HSMul.hSMul (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) g
                      (Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) P))
                  x hx) :
              G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
          HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
        (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P)
⊢ Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) Q =
    HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯ :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P)

Tactic:
obtain ⟨x, hx⟩ := x