-- Mathlib/FieldTheory/Fixed.lean
theorem toAlgAut_surjective [Finite G] :
    Function.Surjective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F)

Proof state:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
⊢ (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯ →
    ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Tactic:
refine QuotientGroup.induction_on q (fun g hg ↦ ⟨g, ?_⟩)

Result:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
g : G
hg : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) ↑g = AlgEquiv.ofRingEquiv ⋯
⊢ (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) g = f

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
this : FaithfulSMul Q F
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
intro f

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
g₁ g₂ : G
h : ∀ (a : F), Quotient.mk'' g₁ • a = Quotient.mk'' g₂ • a
⊢ g₁⁻¹ * g₂ ∈ f.ker

Tactic:
rwa [MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]

Result:
no goals

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Tactic:
obtain ⟨q, hq⟩ := (toAlgAut_bijective Q F).surjective
  (AlgEquiv.ofRingEquiv (f := f) (fun ⟨x, hx⟩ ↦ f.commutes' ⟨x, fun g ↦ hx g⟩))

Result:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
hq : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
let Q := G ⧸ f.ker

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
let _ : MulSemiringAction Q F := MulSemiringAction.compHom _ (QuotientGroup.kerLift f)

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Proof state:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
hq : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯
⊢ ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Tactic:
revert hq

Result:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
⊢ (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) q = AlgEquiv.ofRingEquiv ⋯ →
    ∃ a, (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) a = f

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂

Tactic:
refine Quotient.inductionOn₂' q₁ q₂ (fun g₁ g₂ h ↦ QuotientGroup.eq.mpr ?_)

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
g₁ g₂ : G
h : ∀ (a : F), Quotient.mk'' g₁ • a = Quotient.mk'' g₂ • a
⊢ g₁⁻¹ * g₂ ∈ f.ker

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
⊢ ∀ {m₁ m₂ : Q}, (∀ (a : F), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
intro q₁ q₂

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
q₁ q₂ : Q
⊢ (∀ (a : F), q₁ • a = q₂ • a) → q₁ = q₂