awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ :
  ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
      σ =
    l
intro :
  ∀ (x : S),
    HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x : S)
        (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
      Q
⊢ ∃ (σ : G), IsArithFrobAt R σ Q

Tactic:
refine ⟨σ, fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ :
  ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
      σ =
    l
x : S
intro :
  Eq (α := S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x) : S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) (x ^ p ^ (↑k : ℕ)) : S ⧸ Q)
⊢ HSub.hSub (α := S) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x : S)
      (x ^ Nat.card.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R Q))) ∈
    Q

Tactic:
rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]

Premises used: Ideal.Quotient.eq, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ :
  ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
      σ =
    l
x : S
⊢ Eq (α := S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x) : S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) (x ^ p ^ (↑k : ℕ)) : S ⧸ Q)

Tactic:
DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)

Premises used: DFunLike.congr_fun, Quotient.liftOn', Ideal.Quotient.mk, AddCon.liftOn, Submodule.Quotient.mk, Quot.map, Quotient.map', DFunLike.coe
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this_1 : Algebra.IsIntegral R S
this_2 : Q.IsMaximal
p : ℕ
hc : CharP.{u_1} (R ⧸ P) p
this_3 : Finite.{u_1 + 1} (R ⧸ P)
val : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card.{u_1} (R ⧸ P) = p ^ (↑k : ℕ)
this_4 : CharP.{u_2} (S ⧸ Q) p
this : ExpChar.{u_2} (S ⧸ Q) p
l : Gal((S ⧸ Q)/R ⧸ P) :=
  let __spread.0 : S ⧸ Q ≃+* S ⧸ Q := iterateFrobeniusEquiv (S ⧸ Q) p (↑k : ℕ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ :
  ((Ideal.Quotient.stabilizerHom Q P G : MonoidHom.{u_3, u_2} ↥(MulAction.stabilizer G Q) Gal((S ⧸ Q)/R ⧸ P)) :
        (a : ↥(MulAction.stabilizer G Q)) → Gal((S ⧸ Q)/R ⧸ P))
      σ =
    l
x : S
⊢ Eq (α := S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) ((MulSemiringAction.toAlgHom R S (↑σ : G) : (a : S) → S) x) : S ⧸ Q)
    ((Ideal.Quotient.mk Q : (a : S) → S ⧸ Q) (x ^ p ^ (↑k : ℕ)) : S ⧸ Q)

Tactic:
exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)

Premises used: DFunLike.congr_fun, Ideal.Quotient.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
hP : ∃ (Q : (↑(P.primesOver S) : Type u_2)), Finite.{u_2 + 1} (S ⧸ (↑Q : Ideal S))
obtain :
  ∀ (Q : Ideal S) (hQ₁ : Q.IsPrime) (hQ₂ : Q.LiesOver P)
    (hQ₃ :
      Finite.{u_2 + 1}
        (S ⧸
          (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) :
            Ideal S))),
    ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)

Tactic:
obtain ⟨⟨Q, hQ₁, hQ₂⟩, hQ₃⟩ := hP
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
⊢ ∀ (Q' : (↑(P.primesOver S) : Type u_2)), ∃ (σ : G), (↑Q' : Ideal S) = σ • 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)
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
this : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), ∃ (σ : G), (↑Q' : Ideal S) = σ • Q
choose :
  ∀ (τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G)
    (hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q),
    ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)

Tactic:
choose τ hτ using this
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G
hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q
obtain :
  ∀ (σ : G) (hσ : IsArithFrobAt R σ Q),
    ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)

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

Premises used: IsArithFrobAt.exists_of_isInvariant
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G
hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)

Tactic:
⟨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⟩)⟩

Premises used: Iff.mpr, isConj_iff, IsConj.symm, HMul.hMul, IsConj.trans, Eq.rec, Inv.inv, And.intro, Exists.intro, Eq.symm, IsArithFrobAt.conj, rfl
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G
hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q
σ : G
hσ : IsArithFrobAt R σ Q
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), 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⟩)⟩
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
⊢ IsArithFrobAt R (arithFrobAt R G Q) Q

Tactic:
(exists_primesOver_isConj S G (Q.under R)
    ⟨⟨Q, ‹_›, ⟨rfl⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.1 ⟨Q, ‹_›, ⟨rfl⟩⟩

Premises used: Exists.choose_spec, IsArithFrobAt.exists_primesOver_isConj, Ideal.LiesOver.mk, Subtype.mk, arithFrobAt, And.left, And.intro, Exists.intro, rfl, Ideal.under
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
⊢ Membership.mem (γ := Subgroup G) (MulAction.stabilizer G Q) (arithFrobAt R G Q)

Tactic:
mem_stabilizer (.arithFrobAt R G Q)

Premises used: IsArithFrobAt.mem_stabilizer, IsArithFrobAt.arithFrobAt
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
⊢ ∃ (P : Ideal R), P.IsPrime ∧ P = Ideal.under R Q ∧ P = Ideal.under R Q'

Tactic:
⟨Q.under R, inferInstance, rfl, H⟩

Premises used: inferInstance, And.intro, Exists.intro, rfl, Ideal.under
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
obtain :
  ∀ (P : Ideal R) (hP : P.IsPrime) (h₁ : P = Ideal.under R Q) (h₂ : P = Ideal.under R Q'),
    IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
⊢ IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')

Tactic:
obtain ⟨P, hP, h₁, h₂⟩ : ∃ P : Ideal R, P.IsPrime ∧ P = Q.under R ∧ P = Q'.under R :=
    ⟨Q.under R, inferInstance, rfl, H⟩

Premises used: Ideal, Ideal.under
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ IsConj (α := G)
    (Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
        (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
          ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
        ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) :
      G)
    (Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
        (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
          ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
        ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q' ⋯) :
      G)

Tactic:
(exists_primesOver_isConj S G P ⟨⟨Q, ‹_›, ⟨h₁⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.2 ⟨Q, ‹_›, ⟨h₁⟩⟩
      ⟨Q', ‹_›, ⟨h₂⟩⟩

Premises used: Exists.choose_spec, IsArithFrobAt.exists_primesOver_isConj, Ideal.LiesOver.mk, Subtype.mk, And.right, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
h :
  arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯)
h₃ :
  arithFrobAt R G Q' =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q' ⋯)
⊢ IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')

Tactic:
convert!
    (exists_primesOver_isConj S G P ⟨⟨Q, ‹_›, ⟨h₁⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.2 ⟨Q, ‹_›, ⟨h₁⟩⟩
      ⟨Q', ‹_›, ⟨h₂⟩⟩

Premises used: Exists.choose_spec, IsArithFrobAt.exists_primesOver_isConj, Ideal.LiesOver.mk, Subtype.mk, And.right, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
h :
  ∀ (hP : Ideal.IsPrime (Ideal.under R Q)) (h₂ : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')),
    arithFrobAt R G Q =
      Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2) → G) ↦
        (∀ (Q_1 : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsArithFrobAt R (σ Q_1) (↑Q_1 : Ideal S)) ∧
          ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
        ⋯
        (Subtype.mk (p := fun (x : Ideal S) ↦
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) x) Q ⋯)
⊢ arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯)

Tactic:
subst h₁
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
hP : Ideal.IsPrime (Ideal.under R Q)
h₂ : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
⊢ arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2) → G) ↦
      (∀ (Q_1 : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsArithFrobAt R (σ Q_1) (↑Q_1 : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯
      (Subtype.mk (p := fun (x : Ideal S) ↦
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) x) Q ⋯)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
h :
  ∀ (hP : Ideal.IsPrime (Ideal.under R Q')) (h₁ : Eq (α := Ideal R) (Ideal.under R Q') (Ideal.under R Q)),
    arithFrobAt R G Q' =
      Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2) → G) ↦
        (∀ (Q : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
          ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
        ⋯
        (Subtype.mk (p := fun (x : Ideal S) ↦
          Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q') S) x) Q' ⋯)
⊢ arithFrobAt R G Q' =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q' ⋯)

Tactic:
subst h₂
-- Module: Mathlib.RingTheory.Frobenius
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
hP : Ideal.IsPrime (Ideal.under R Q')
h₁ : Eq (α := Ideal R) (Ideal.under R Q') (Ideal.under R Q)
⊢ arithFrobAt R G Q' =
    Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2) → G) ↦
      (∀ (Q : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯
      (Subtype.mk (p := fun (x : Ideal S) ↦
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q') S) x) Q' ⋯)

Tactic:
rfl