-- Mathlib/RingTheory/Invariant.lean
theorem Ideal.Quotient.stabilizerHom_surjective :
    Function.Surjective (Ideal.Quotient.stabilizerHom Q P G)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
have key := IsFractionRing.stabilizerHom_surjective G P Q
  (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q))

Result:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key : Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key : Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
rw [IsFractionRing.stabilizerHom, MonoidHom.coe_comp] at key

Result:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key :
  Function.Surjective
    (⇑(IsFractionRing.fieldEquivOfAlgEquivHom (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q))) ∘ ⇑(stabilizerHom Q P G))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
key :
  Function.Surjective
    (⇑(IsFractionRing.fieldEquivOfAlgEquivHom (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q))) ∘ ⇑(stabilizerHom Q P G))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
exact key.of_comp_left (IsFractionRing.fieldEquivOfAlgEquivHom_injective (A ⧸ P) (B ⧸ Q)
  (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q

Result:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Proof state:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
⊢ Function.Surjective ⇑(stabilizerHom Q P G)

Tactic:
let _ := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))

Result:
A : Type u_1
B : Type u_2
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Finite G
inst✝⁴ : MulSemiringAction G B
inst✝³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : Algebra.IsInvariant A B G
this : P.IsPrime
x✝ : Algebra (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)) := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
⊢ Function.Surjective ⇑(stabilizerHom Q P G)