Exists of is Invariant of profinite

lemma exists_of_isInvariant_of_profinite    [Q.IsMaximal] [Finite (R ⧸ Q.under R)] : ∃ σ : G, IsArithFrobAt R σ Q := by  letI : TopologicalSpace S := ⊥  letI : DiscreteTopology S := ⟨rfl⟩  let P := Q.under R  have : Algebra.IsIntegral R S := Algebra.IsInvariant.isIntegral_of_profinite (G := G)  -- have : Q.IsMaximal := Ideal.Quotient.maximal_of_isField _ (Finite.isField_of_domain (S ⧸ Q))  have : P.IsMaximal := Ideal.isMaximal_comap_of_isIntegral_of_isMaximal Q  obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)  -- have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective  cases nonempty_fintype (R ⧸ P)  obtain ⟨k, hp, hk⟩ := FiniteField.card (R ⧸ P) p  have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero  have : ExpChar (S ⧸ Q) p := .prime hp  have : PerfectField (S ⧸ Q) := Algebra.IsAlgebraic.perfectField (K := (R ⧸ P))  let l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=    { __ := iterateFrobeniusEquiv (S ⧸ Q) p k,      commutes' r := by        dsimp [iterateFrobenius_def]        rw [← map_pow, ← hk, FiniteField.pow_card] }  obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective_of_profinite (G := G) P Q l  refine ⟨σ, fun x ↦ ?_⟩  rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]  exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)