-- Mathlib/RingTheory/Frobenius.lean
lemma exists_primesOver_isConj (P : Ideal R)
    (hP : ∃ Q : Ideal.primesOver P S, Finite (S ⧸ Q.1)) :
    ∃ σ : Ideal.primesOver P S → G, (∀ Q, IsArithFrobAt R (σ Q) Q.1) ∧
      (∀ Q₁ Q₂, IsConj (σ Q₁) (σ Q₂))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
hP : ∃ Q, Finite (S ⧸ ↑Q)
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
obtain ⟨⟨Q, hQ₁, hQ₂⟩, hQ₃⟩ := hP

Result:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Proof state:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
obtain ⟨σ, hσ⟩ := exists_of_isInvariant R G Q

Result:
case intro.mk.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Proof state:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
this : ∀ (Q' : ↑(P.primesOver S)), ∃ σ, ↑Q' = σ • Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
choose τ hτ using this

Result:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Proof state:
case intro.mk.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
τ : ↑(P.primesOver S) → G
hτ : ∀ (Q' : ↑(P.primesOver S)), ↑Q' = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
refine ⟨fun Q' ↦ τ Q' * σ * (τ Q')⁻¹, fun Q' ↦ hτ Q' ▸ hσ.conj (τ Q'), fun Q₁ Q₂ ↦
  .trans (.symm (isConj_iff.mpr ⟨τ Q₁, rfl⟩)) (isConj_iff.mpr ⟨τ Q₂, rfl⟩)⟩

Result:
no goals

Proof state:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

Tactic:
have (Q' : Ideal.primesOver P S) : ∃ σ : G, Q'.1 = σ • Q :=
  Algebra.IsInvariant.exists_smul_of_under_eq R S G _ _ (hQ₂.over.symm.trans Q'.2.2.over)

Result:
case intro.mk.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
inst✝¹ : Finite G
inst✝ : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ : Finite (S ⧸ ↑⟨Q, ⋯⟩)
this : ∀ (Q' : ↑(P.primesOver S)), ∃ σ, ↑Q' = σ • Q
⊢ ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)