Theorem: orbit_stabilizer (FormalBook/Chapter_06.lean)

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI := Fintype.ofFinite (Set.centralizer {ConjClasses.exists_rep A|>.choose})
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI : Fintype ↑(MulAction.orbit (ConjAct Rˣ) (ConjClasses.exists_rep A|>.choose))
    := by refine Set.fintypeRange fun m => m • Exists.choose ?_
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
letI : Fintype { x // x ∈ MulAction.stabilizer (ConjAct Rˣ)
      (ConjClasses.exists_rep A|>.choose) } := Fintype.ofFinite _
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝¹ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝¹ : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
have := MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct Rˣ)
    (ConjClasses.exists_rep A|>.choose)
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) =
    Fintype.card (ConjAct Rˣ)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) =
    Fintype.card (ConjAct Rˣ)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
replace this := this.symm
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↑{⋯.choose}.centralizer
Tactic:
rw [Fintype.card_congr <| ConjAct_stabilizer_centralizer_eq (ConjClasses.exists_rep A|>.choose)]
State after:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ Fintype.card Rˣ = Fintype.card ↑A.carrier * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
Tactic:
convert this
State after:
case h.e'_3.h.e'_5.h.h.e'_2
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ A.carrier = MulAction.orbit (ConjAct Rˣ) ⋯.choose

State before:
case h.e'_3.h.e'_5.h.h.e'_2
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this✝² : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
this✝¹ : Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) := Set.fintypeRange fun m => m • ⋯.choose
this✝ : Fintype ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose) :=
  Fintype.ofFinite ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
this :
  Fintype.card (ConjAct Rˣ) =
    Fintype.card ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose) * Fintype.card ↥(MulAction.stabilizer (ConjAct Rˣ) ⋯.choose)
⊢ A.carrier = MulAction.orbit (ConjAct Rˣ) ⋯.choose
Tactic:
rw [ConjAct.orbit_eq_carrier_conjClasses, (ConjClasses.exists_rep A|>.choose_spec)]
State after:
no goals

State before:
R : Type u_1
inst✝³ : DecidableEq R
inst✝² : DivisionRing R
inst✝¹ : Fintype R
A : ConjClasses Rˣ
inst✝ : Fintype ↑A.carrier
this : Fintype ↑{⋯.choose}.centralizer := Fintype.ofFinite ↑{⋯.choose}.centralizer
⊢ Fintype ↑(MulAction.orbit (ConjAct Rˣ) ⋯.choose)
Tactic:
refine Set.fintypeRange fun m => m • Exists.choose ?_
State after:
no goals