awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
h : B' ↥(↑N'.toOpenSubgroup : Subgroup G) ≤ B' ↥(↑N.toOpenSubgroup : Subgroup G)
x : G
hx :
  Ideal.under (↥(B' ↥(↑N.toOpenSubgroup : Subgroup G))) Q =
    HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β := Ideal ↥(B' ↥(↑N.toOpenSubgroup : Subgroup G)))
      (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (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 : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) hx) :
            G ⧸ (↑N.toOpenSubgroup : Subgroup G)) :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (Ideal.under (↥(B' ↥(↑N'.toOpenSubgroup : Subgroup G))) P)

Tactic:
simpa only [Ideal.comap_comap, Ideal.pointwise_smul_eq_comap, ← Ideal.comap_coe
        (F := RingEquiv _ _)] using congr(Ideal.comap (Subalgebra.inclusion h).toRingHom $hx)

Premises used: Ideal.pointwise_smul_eq_comap, Ideal.comap_coe, Ideal.comap_comap
-- 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
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { 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) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (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) }) ↦
        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))
          ((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)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
N : OpenNormalSubgroup G
obtain :
  ∀ (g : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
    (hg :
      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)),
    Nonempty.{u + 1} (F.obj N)
⊢ Nonempty.{u + 1} (F.obj N)

Tactic:
obtain ⟨g, hg⟩ := Algebra.IsInvariant.exists_smul_of_under_eq A
      (B' N.1.1) (G ⧸ N.1.1) (P.under _) (Q.under _) hPQ

Premises used: Algebra.IsInvariant.exists_smul_of_under_eq, Membership.mem, Subtype, HasQuotient.Quotient, OpenNormalSubgroup.toOpenSubgroup, OpenSubgroup.toSubgroup, Ideal.under
-- 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
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { 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) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (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) }) ↦
        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))
          ((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)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
N : OpenNormalSubgroup G
g : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hg :
  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)
⊢ Nonempty.{u + 1} (F.obj N)

Tactic:
⟨g, hg⟩

Premises used: Nonempty.intro, Subtype.mk
-- 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
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { 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) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (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) }) ↦
        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))
          ((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)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
N : OpenNormalSubgroup G
g : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hg :
  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)
⊢ Nonempty.{u + 1} (F.obj N)

Tactic:
exact ⟨g, hg⟩
-- 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
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { 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) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (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) }) ↦
        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))
          ((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)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
⊢ ∀ (N : OpenNormalSubgroup G), Nonempty.{u + 1} (F.obj N)

Tactic:
have (N : _) : Nonempty (F.obj N) := by
    obtain ⟨g, hg⟩ := Algebra.IsInvariant.exists_smul_of_under_eq A
      (B' N.1.1) (G ⧸ N.1.1) (P.under _) (Q.under _) hPQ
    exact ⟨g, hg⟩
-- 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
F : OpenNormalSubgroup G ⥤ Type u :=
  {
    obj := fun (N : OpenNormalSubgroup G) ↦
      { 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) },
    map := fun {N N' : OpenNormalSubgroup G} (f : N ⟶ N') ↦
      ↾fun
          (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) }) ↦
        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))
          ((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)))
          ⋯,
    map_id := ⋯, map_comp := ⋯ }
this : ∀ (N : OpenNormalSubgroup G), Nonempty.{u + 1} (F.obj N)
obtain : ∀ (s : (j : OpenNormalSubgroup G) → F.obj j) (hs : s ∈ F.sections), ∃ (g : G), Q = g • P
⊢ ∃ (g : G), Q = g • P

Tactic:
obtain ⟨s, hs⟩ := nonempty_sections_of_finite_cofiltered_system F

Premises used: nonempty_sections_of_finite_cofiltered_system
-- 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
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    x
⊢ LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))

Tactic:
have h : FixedPoints.subalgebra A B N'.1.1 ≤ FixedPoints.subalgebra A B N.1.1 :=
    fun x hx n ↦ hx ⟨_, e 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
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
x : G ⧸ (↑N.toOpenSubgroup : Subgroup G)
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    x
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
obtain :
  ∀ (x : G)
    (hx :
      Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
        (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
          Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
          (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
        (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))),
    HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
        ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
              (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)
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
      under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q
⊢ HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (a : G ⧸ (↑N.toOpenSubgroup : Subgroup G)) → G ⧸ N'.toOpenSubgroup.1)
          x :
        HasQuotient.Quotient G (B := Subgroup G) N'.toOpenSubgroup.1)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x

Premises used: QuotientGroup.mk_surjective, rfl
-- 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
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
x : G
hx :
  Membership.mem (γ := Subgroup (G ⧸ (↑N.toOpenSubgroup : Subgroup G)))
    (MulAction.stabilizer (G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (α :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
⊢ Eq (α := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
    (comap (Subalgebra.inclusion h)
      (HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)))
    (comap (Subalgebra.inclusion h)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))

Tactic:
replace hx := congr(Ideal.comap (Subalgebra.inclusion h) $hx)
-- 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
Q : Ideal B
N N' : OpenNormalSubgroup G
e : N ≤ N'
h :
  LE.le (α := Subalgebra A B) (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))
    (FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))
x : G
hx :
  Eq (α := Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
    (comap (Subalgebra.inclusion h)
      (HSMul.hSMul (α := G ⧸ (↑N.toOpenSubgroup : Subgroup G)) (β :=
        Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
        (↑x : G ⧸ (↑N.toOpenSubgroup : Subgroup G))
        (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q)))
    (comap (Subalgebra.inclusion h)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
⊢ HSMul.hSMul (α := G ⧸ (↑N'.toOpenSubgroup : Subgroup G)) (β :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G)))
      ((QuotientGroup.map (↑N.toOpenSubgroup : Subgroup G) N'.toOpenSubgroup.1 (MonoidHom.id G) e :
            (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)
      (under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q) =
    under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N'.toOpenSubgroup : Subgroup G))) Q

Tactic:
simpa only [Ideal.pointwise_smul_eq_comap,
    ← Ideal.comap_coe (F := RingEquiv _ _), Ideal.comap_comap] using hx

Premises used: Ideal.pointwise_smul_eq_comap, Ideal.comap_coe, Ideal.comap_comap
-- 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
P_1 : Ideal A
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
P : Ideal A
Q : Ideal B
inst_13 : Q.IsPrime
inst_14 : Q.LiesOver P
inst_15 : Algebra.IsInvariant A B G
σ : AlgEquiv.{u_1, u_2, u_2} (A ⧸ P) (B ⧸ Q) (B ⧸ Q)
N : OpenNormalSubgroup G
⊢ IsScalarTower.{u_1, u_2, u_2} (A ⧸ P)
    (HasQuotient.Quotient ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)) (B :=
      Ideal ↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G)))
      (Ideal.under (↥(FixedPoints.subalgebra.{u_1, u_2, u} A B ↥(↑N.toOpenSubgroup : Subgroup G))) Q))
    (B ⧸ Q)

Tactic:
have : IsScalarTower (A ⧸ P) (FixedPoints.subalgebra A B N.1.1 ⧸
    Q.under (FixedPoints.subalgebra A B N.1.1)) (B ⧸ Q) := IsScalarTower.of_algebraMap_eq
    (Quotient.ind fun x ↦ rfl)
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
x : R
⊢ Eq.{v + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S)
    ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) x : R[X]) : S)

Tactic:
AlgHom.algebraMap_eq_apply h.map rfl

Premises used: AlgHom.algebraMap_eq_apply, IsAdjoinRoot.map, rfl
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
rw : Membership.mem (γ := Ideal R[X]) (Ideal.span {f}) p ↔ f ∣ p
rw₁ rw₂ : f ∣ p ↔ f ∣ p
⊢ Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) p ↔ f ∣ p

Tactic:
rw [h.ker_map, Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton, IsAdjoinRoot.ker_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
p : R[X]
⊢ Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) p : S) (0 : S) ↔ f ∣ p

Tactic:
simpa using h.mem_ker_map

Premises used: IsAdjoinRoot.mem_ker_map
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRoot S f
⊢ (h.map : (a : R[X]) → S) X = h.root

Tactic:
rfl

Premises used: IsAdjoinRoot.root, rfl