awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨b, rfl⟩ := hAB.isInvariant b
    (by simpa [ha, hxy, smul_div₀', ← algebraMap.coe_smul'] using h)
Cleared hypotheses: b, hb, hxy
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use algebraMap A K b / algebraMap A K a
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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)
⊢ (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)
have 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) ((algebraMap A B : (a : A) → B) b : B) : L)
    ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
Tactic: rw [hxy, map_div₀, hc, hc]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
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) ((algebraMap A B : (a : A) → B) b : B) : L)
      ((algebraMap B L : (a : B) → L) ((algebraMap A B : (a : A) → B) a : B) : L)
⊢ (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)
have h₂ : HDiv.hDiv (α := L) (β := L) ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) b : K) : L)
    ((algebraMap K L : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : 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)
Tactic: rw [hxy, map_div₀, hc, hc]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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
⊢ Algebra.IsIntegral A B
have isIntegral : ∀ (x : B), IsIntegral A x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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 A x
have isIntegral : ∀ (N : OpenNormalSubgroup G) (hN : (↑N : Set G) ⊆ (↑(MulAction.stabilizer G x) : Set G)), IsIntegral A x
Tactic: obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
    (stabilizer_isOpen G x) (one_mem _)
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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 x
have 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 sorry)
Tactic: have := (Algebra.IsInvariant.isIntegral A (FixedPoints.subalgebra A B N.1.1) (G ⧸ N.1.1)).1
    ⟨x, fun g ↦ hN g.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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) }
⊢ 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)
have h : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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)
⊢ 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)
have 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) sorry :
            (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)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Profinite (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
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 := ⋯ }
⊢ ∃ (g : G), Q = g • P
have this : ∀ (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⟩