Theorem: lagrange_theorem (RSAProject/rsaproject.lean)

State before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h : x ∈ H
⊢ { val := x, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
obtain ⟨n, h⟩ := Subgroup.mem_closure_singleton.mp h
State after:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h✝ : x ∈ H
n : ℤ
h : a ^ n = x
⊢ { val := x, property := h✝ } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }

State before:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h✝ : x ∈ H
n : ℤ
h : a ^ n = x
⊢ { val := x, property := h✝ } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
subst h
State after:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
n : ℤ
h : a ^ n ∈ H
⊢ { val := a ^ n, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }

State before:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
n : ℤ
h : a ^ n ∈ H
⊢ { val := a ^ n, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
sorry
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ orderOf a ∣ Fintype.card α
Tactic:
rw [←this]
State after:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ Fintype.card { x // x ∈ H } ∣ Fintype.card α

State before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ Fintype.card { x // x ∈ H } ∣ Fintype.card α
Tactic:
apply Subgroup.card_subgroup_dvd_card
State after:
no goals