[GOAL]
n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)
[PROOFSTEP]
rintro (i | i) (j | j) (k | k)
[GOAL]
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * a k = a i * (a j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * xa k = a i * (a j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * a k = a i * (xa j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * xa k = a i * (xa j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * a k = xa i * (a j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * xa k = xa i * (a j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * a k = xa i * (xa j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * xa k = xa i * (xa j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)
[PROOFSTEP]
ring_nf
[GOAL]
case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)
[PROOFSTEP]
ring_nf
[GOAL]
case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (j - i)) = a (i + (↑n + k - j))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (i + j)) = a (↑n + (k - j) - i)
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + j - i + k) = a (↑n + (j + k) - i)
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n + j - i)) = xa (i + (↑n + k - j))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k + (-↑n - j) + i) = xa (k + (↑n - j) + i)
[PROOFSTEP]
congr
[GOAL]
case xa.xa.xa.e_a.e_a.e_a.e_a
n : ℕ
i j k : ZMod (2 * n)
⊢ -↑n = ↑n
[PROOFSTEP]
calc
  -(n : ZMod (2 * n)) = 0 - n := by rw [zero_sub]
  _ = 2 * n - n := by norm_cast; simp
  _ = n := by ring
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ -↑n = 0 - ↑n
[PROOFSTEP]
rw [zero_sub]
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ 0 - ↑n = 2 * ↑n - ↑n
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ ↑(Int.subNatNat 0 n) = ↑(Int.subNatNat (2 * n) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ 2 * ↑n - ↑n = ↑n
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), 1 * a = a
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i
[PROOFSTEP]
exact congr_arg a (zero_add i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i
[PROOFSTEP]
exact congr_arg xa (sub_zero i)
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), a * 1 = a
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i
[PROOFSTEP]
exact congr_arg a (add_zero i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i
[PROOFSTEP]
exact congr_arg xa (add_zero i)
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), a⁻¹ * a = 1
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ (a i)⁻¹ * a i = 1
[PROOFSTEP]
exact congr_arg a (neg_add_self i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i)⁻¹ * xa i = 1
[PROOFSTEP]
exact congr_arg a (sub_self (n + i))
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case a
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i =>
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (a x)) =
    a x
[PROOFSTEP]
rfl
[GOAL]
case xa
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i =>
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (xa x)) =
    xa x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun i =>
    match i with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j
[PROOFSTEP]
rintro (k | k)
[GOAL]
case a
n : ℕ
k : ZMod (2 * 0)
⊢ (fun i =>
        match i with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (a k)) =
    a k
[PROOFSTEP]
rfl
[GOAL]
case xa
n : ℕ
k : ZMod (2 * 0)
⊢ (fun i =>
        match i with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (xa k)) =
    xa k
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun i =>
    match i with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j
[PROOFSTEP]
rintro (k | k)
[GOAL]
case r
n : ℕ
k : ZMod 0
⊢ (fun i =>
        match i with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.r k)) =
    DihedralGroup.r k
[PROOFSTEP]
rfl
[GOAL]
case sr
n : ℕ
k : ZMod 0
⊢ (fun i =>
        match i with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∀ (x y : QuaternionGroup 0),
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (x * y) =
      Equiv.toFun
          {
            toFun := fun i =>
              match i with
              | a j => DihedralGroup.r j
              | xa j => DihedralGroup.sr j,
            invFun := fun i =>
              match i with
              | DihedralGroup.r j => a j
              | DihedralGroup.sr j => xa j,
            left_inv :=
              (_ :
                ∀ (x : QuaternionGroup 0),
                  (fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      ((fun i =>
                          match i with
                          | a j => DihedralGroup.r j
                          | xa j => DihedralGroup.sr j)
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DihedralGroup 0),
                  (fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      ((fun i =>
                          match i with
                          | DihedralGroup.r j => a j
                          | DihedralGroup.sr j => xa j)
                        x) =
                    x) }
          x *
        Equiv.toFun
          {
            toFun := fun i =>
              match i with
              | a j => DihedralGroup.r j
              | xa j => DihedralGroup.sr j,
            invFun := fun i =>
              match i with
              | DihedralGroup.r j => a j
              | DihedralGroup.sr j => xa j,
            left_inv :=
              (_ :
                ∀ (x : QuaternionGroup 0),
                  (fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      ((fun i =>
                          match i with
                          | a j => DihedralGroup.r j
                          | xa j => DihedralGroup.sr j)
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DihedralGroup 0),
                  (fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      ((fun i =>
                          match i with
                          | DihedralGroup.r j => a j
                          | DihedralGroup.sr j => xa j)
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro (k | k) (l | l)
[GOAL]
case a.a
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (a k * a l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a l)
[PROOFSTEP]
simp
[GOAL]
case a.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (a k * xa l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa l)
[PROOFSTEP]
simp
[GOAL]
case xa.a
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (xa k * a l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a l)
[PROOFSTEP]
simp
[GOAL]
case xa.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (xa k * xa l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa l)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ a 0 ≠ xa 0
[PROOFSTEP]
revert n
[GOAL]
⊢ ∀ {n : ℕ}, a 0 ≠ xa 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n
[PROOFSTEP]
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
⊢ a 1 ^ k = a ↑k
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
n : ℕ
⊢ a 1 ^ Nat.zero = a ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
n : ℕ
⊢ a 1 ^ Nat.zero = a 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ Nat.succ k = a ↑(Nat.succ k)
[PROOFSTEP]
rw [pow_succ, IH, a_mul_a]
[GOAL]
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a (1 + ↑k) = a ↑(Nat.succ k)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ 1 + ↑k = ↑(Nat.succ k)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ ↑(1 + k) = ↑(Nat.succ k)
[PROOFSTEP]
rw [Nat.one_add]
[GOAL]
n : ℕ
⊢ a 1 ^ (2 * n) = 1
[PROOFSTEP]
rw [a_one_pow, one_def]
[GOAL]
n : ℕ
⊢ a ↑(2 * n) = a 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ ↑(2 * n) = 0
[PROOFSTEP]
exact ZMod.nat_cast_self _
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 2 = a ↑n
[PROOFSTEP]
simp [sq]
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = 1
[PROOFSTEP]
rw [pow_succ, pow_succ, sq, xa_mul_xa, xa_mul_a, xa_mul_xa, add_sub_cancel, add_sub_assoc, add_sub_cancel']
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = 1
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(n + n) = 1
[PROOFSTEP]
rw [← two_mul]
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1
[PROOFSTEP]
simp [one_def]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 4
[PROOFSTEP]
change _ = 2 ^ 2
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 2 ^ 2
[PROOFSTEP]
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = 2 ^ 2
[PROOFSTEP]
apply orderOf_eq_prime_pow
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1
[PROOFSTEP]
intro h
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ 2 ^ 1 = 1
⊢ False
[PROOFSTEP]
simp only [pow_one, xa_sq] at h
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : a ↑n = 1
⊢ False
[PROOFSTEP]
injection h with h'
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ↑n = 0
⊢ False
[PROOFSTEP]
apply_fun ZMod.val at h'
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val ↑n = ZMod.val 0
⊢ False
[PROOFSTEP]
apply_fun (· / n) at h'
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val ↑n / n = ZMod.val 0 / n
⊢ False
[PROOFSTEP]
simp only [ZMod.val_nat_cast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self, Nat.div_self (NeZero.pos n)] at h'
[GOAL]
case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ IsCyclic (QuaternionGroup 1)
[PROOFSTEP]
apply isCyclic_of_orderOf_eq_card
[GOAL]
case hx
n : ℕ
⊢ orderOf ?x = Fintype.card (QuaternionGroup 1)
case x n : ℕ ⊢ QuaternionGroup 1
[PROOFSTEP]
rw [card, mul_one]
[GOAL]
case hx
n : ℕ
⊢ orderOf ?x = 4
case x
n : ℕ
⊢ QuaternionGroup 1
case x
n : ℕ
⊢ QuaternionGroup 1
case x n : ℕ ⊢ QuaternionGroup 1
[PROOFSTEP]
exact orderOf_xa 0
[GOAL]
n : ℕ
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
cases' eq_zero_or_neZero n with hn hn
[GOAL]
case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
subst hn
[GOAL]
case inl
⊢ orderOf (a 1) = 2 * 0
[PROOFSTEP]
simp_rw [mul_zero, orderOf_eq_zero_iff']
[GOAL]
case inl
⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1
[PROOFSTEP]
intro n h
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1
[PROOFSTEP]
rw [one_def, a_one_pow]
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0
[PROOFSTEP]
apply mt a.inj
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0
[PROOFSTEP]
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
[GOAL]
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0
[PROOFSTEP]
simpa using h.ne'
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
apply (Nat.le_of_dvd (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n
[PROOFSTEP]
intro h
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False
[PROOFSTEP]
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False
[PROOFSTEP]
rw [a_one_pow] at h1
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
[PROOFSTEP]
injection h1 with h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False
[PROOFSTEP]
rw [← ZMod.val_eq_zero, ZMod.val_nat_cast, Nat.mod_eq_of_lt h] at h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False
[PROOFSTEP]
exact absurd h2.symm (orderOf_pos _).ne
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
[PROOFSTEP]
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑(ZMod.val i)) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
[PROOFSTEP]
rw [← a_one_pow, orderOf_pow, orderOf_a_one]
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2
[PROOFSTEP]
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) (2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
cases' eq_zero_or_neZero n with hn hn
[GOAL]
case inl
n : ℕ
hn : n = 0
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
subst hn
[GOAL]
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4
[PROOFSTEP]
simp only [lcm_zero_left, mul_zero]
[GOAL]
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = 0
[PROOFSTEP]
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4
[PROOFSTEP]
apply Monoid.exponent_dvd_of_forall_pow_eq_one
[GOAL]
case inr.a.hG
n : ℕ
hn : NeZero n
⊢ ∀ (g : QuaternionGroup n), g ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rintro (m | m)
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / Nat.gcd (2 * n) (ZMod.val m) ∣ lcm (2 * n) 4
[PROOFSTEP]
refine' Nat.dvd_trans ⟨gcd (2 * n) m.val, _⟩ (dvd_lcm_left (2 * n) 4)
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / Nat.gcd (2 * n) (ZMod.val m) * gcd (2 * n) (ZMod.val m)
[PROOFSTEP]
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm
[GOAL]
case inr.a.hG.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
[GOAL]
case inr.a.hG.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ lcm (2 * n) 4
[PROOFSTEP]
exact dvd_lcm_right (2 * n) 4
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (a 1)
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (a 1)
[PROOFSTEP]
exact orderOf_a_one.symm
[GOAL]
case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (xa 0)
[PROOFSTEP]
exact (orderOf_xa 0).symm


[GOAL]
n : ℕ
p : Fin (n + 1)
⊢ ↑decomposeFin.symm (p, Equiv.refl (Fin n)) = swap 0 p
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]
[GOAL]
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑(↑decomposeFin.symm (p, e)) 0 = p
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin]
[GOAL]
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (p, e)) (Fin.succ x) = ↑(swap 0 p) (Fin.succ (↑e x))
[PROOFSTEP]
refine' Fin.cases _ _ p
[GOAL]
case refine'_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ↑(↑decomposeFin.symm (0, e)) (Fin.succ x) = ↑(swap 0 0) (Fin.succ (↑e x))
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, EquivFunctor.map]
[GOAL]
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
by_cases h : i = e x
[GOAL]
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map]
[GOAL]
case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = ↑e x
⊢ ↑(↑decomposeFin.symm (Fin.succ i, e)) (Fin.succ x) = ↑(swap 0 (Fin.succ i)) (Fin.succ (↑e x))
[PROOFSTEP]
simp [h, Fin.succ_ne_zero, Equiv.Perm.decomposeFin, EquivFunctor.map, swap_apply_def, Ne.symm h]
[GOAL]
n : ℕ
e : Perm (Fin (n + 1))
p : Fin (n + 2)
⊢ ↑(↑decomposeFin.symm (p, e)) 1 = ↑(swap 0 p) (Fin.succ (↑e 0))
[PROOFSTEP]
rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]
[GOAL]
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑sign (↑decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
refine' Fin.cases _ _ p
[GOAL]
case refine'_1
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ↑sign (↑decomposeFin.symm (0, e)) = (if 0 = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Fin.succ_ne_zero]
[GOAL]
case refine'_2
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ∀ (i : Fin n), ↑sign (↑decomposeFin.symm (Fin.succ i, e)) = (if Fin.succ i = 0 then 1 else -1) * ↑sign e
[PROOFSTEP]
simp [Equiv.Perm.decomposeFin, Fin.succ_ne_zero]
[GOAL]
n : ℕ
⊢ finRotate (Nat.succ n) = ↑decomposeFin.symm (1, finRotate n)
[PROOFSTEP]
ext i
[GOAL]
case H.h
n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate n)) i)
[PROOFSTEP]
cases n
[GOAL]
case H.h.zero
i : Fin (Nat.succ Nat.zero)
⊢ ↑(↑(finRotate (Nat.succ Nat.zero)) i) = ↑(↑(↑decomposeFin.symm (1, finRotate Nat.zero)) i)
[PROOFSTEP]
simp
[GOAL]
case H.h.succ
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) i) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) i)
[PROOFSTEP]
refine' Fin.cases _ (fun i => _) i
[GOAL]
case H.h.succ.refine'_1
n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) 0) = ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) 0)
[PROOFSTEP]
simp
[GOAL]
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ ↑(↑(finRotate (Nat.succ (Nat.succ n✝))) (Fin.succ i)) =
    ↑(↑(↑decomposeFin.symm (1, finRotate (Nat.succ n✝))) (Fin.succ i))
[PROOFSTEP]
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
[GOAL]
case H.h.succ.refine'_2
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑(Fin.succ i) + 1) = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n✝ : ℕ
i✝ : Fin (Nat.succ (Nat.succ n✝))
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑(Fin.succ i) + 1 = ↑(↑(swap 0 1) (Fin.succ (↑(finRotate (Nat.succ n✝)) i)))
[PROOFSTEP]
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate, if_neg h, Fin.val_zero,
  Fin.val_one, swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
[GOAL]
n : ℕ
⊢ ↑sign (finRotate (n + 1)) = (-1) ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ ↑sign (finRotate (Nat.zero + 1)) = (-1) ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (finRotate (Nat.succ n + 1)) = (-1) ^ Nat.succ n
[PROOFSTEP]
rw [finRotate_succ_eq_decomposeFin]
[GOAL]
case succ
n : ℕ
ih : ↑sign (finRotate (n + 1)) = (-1) ^ n
⊢ ↑sign (↑decomposeFin.symm (1, finRotate (n + 1))) = (-1) ^ Nat.succ n
[PROOFSTEP]
simp [ih, pow_succ]
[GOAL]
n : ℕ
⊢ support (finRotate (n + 2)) = Finset.univ
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ support (finRotate (n + 2)) ↔ a✝ ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ support (finRotate n) = Finset.univ
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ support (finRotate (2 + m)) = Finset.univ
[PROOFSTEP]
rw [add_comm, support_finRotate]
[GOAL]
n : ℕ
⊢ IsCycle (finRotate (n + 2))
[PROOFSTEP]
refine' ⟨0, by simp, fun x hx' => ⟨x, _⟩⟩
[GOAL]
n : ℕ
⊢ ↑(finRotate (n + 2)) 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
x : Fin (n + 2)
hx' : ↑(finRotate (n + 2)) x ≠ x
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
[PROOFSTEP]
clear hx'
[GOAL]
n : ℕ
x : Fin (n + 2)
⊢ ↑(finRotate (n + 2) ^ ↑↑x) 0 = x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(finRotate (n + 2) ^ ↑↑{ val := x, isLt := hx }) 0 = { val := x, isLt := hx }
[PROOFSTEP]
rw [zpow_ofNat, Fin.ext_iff, Fin.val_mk]
[GOAL]
case mk
n x : ℕ
hx : x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
[PROOFSTEP]
induction' x with x ih
[GOAL]
case mk.zero
n x : ℕ
hx✝ : x < n + 2
hx : Nat.zero < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.zero, isLt := hx }) 0) = ↑{ val := Nat.zero, isLt := hx }
[PROOFSTEP]
rfl
[GOAL]
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(↑(finRotate (n + 2) ^ ↑{ val := Nat.succ x, isLt := hx }) 0) = ↑{ val := Nat.succ x, isLt := hx }
[PROOFSTEP]
rw [pow_succ, Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
[GOAL]
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ↑(finRotate (n + 2) ^ x) 0 ≠ Fin.last (n + 1)
[PROOFSTEP]
rw [Ne.def, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
[GOAL]
case mk.succ
n x✝ : ℕ
hx✝ : x✝ < n + 2
x : ℕ
ih : ∀ (hx : x < n + 2), ↑(↑(finRotate (n + 2) ^ ↑{ val := x, isLt := hx }) 0) = ↑{ val := x, isLt := hx }
hx : Nat.succ x < n + 2
⊢ ¬↑{ val := x, isLt := (_ : x < n + 2) } = n + 1
[PROOFSTEP]
exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ IsCycle (finRotate n)
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (2 + m))
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ IsCycle (finRotate (m + 2))
[PROOFSTEP]
exact isCycle_finRotate
[GOAL]
n : ℕ
⊢ cycleType (finRotate (n + 2)) = {n + 2}
[PROOFSTEP]
rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]
[GOAL]
n : ℕ
⊢ ↑[n + 2] = {n + 2}
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
h : 2 ≤ n
⊢ cycleType (finRotate n) = {n}
[PROOFSTEP]
obtain ⟨m, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ cycleType (finRotate (2 + m)) = {2 + m}
[PROOFSTEP]
rw [add_comm, cycleType_finRotate]
[GOAL]
n : ℕ
i : Fin n
⊢ Function.LeftInverse (fun x => ↑↑x) ↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
i : Fin n
x : Fin (Nat.succ ↑i)
⊢ (fun x => ↑↑x) (↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding x) = x
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
i : Fin n
x : Fin (Nat.succ ↑i)
⊢ ↑((fun x => ↑↑x) (↑(castLEEmb (_ : Nat.succ ↑i ≤ n)).toEmbedding x)) = ↑x
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : i < j
⊢ ↑(cycleRange i) j = j
[PROOFSTEP]
rw [cycleRange, ofLeftInverse'_eq_ofInjective, ← Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
  viaFintypeEmbedding_apply_not_mem_range]
[GOAL]
case h
n : ℕ
i j : Fin (Nat.succ n)
h : i < j
⊢ ¬j ∈ Set.range ↑(castLEEmb (_ : Nat.succ ↑i ≤ Nat.succ n)).toEmbedding
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
i j : Fin (Nat.succ Nat.zero)
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
exact
  Subsingleton.elim (α := Fin 1) _
    _
      --Porting note; was `simp`
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt)) ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ := by simp
[GOAL]
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
⊢ j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ ↑(cycleRange i) j = if j = i then 0 else j + 1
[PROOFSTEP]
ext
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ ↑(↑(cycleRange i) j) = ↑(if j = i then 0 else j + 1)
[PROOFSTEP]
erw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ← Function.Embedding.toEquivRange_eq_ofInjective, ←
  viaFintypeEmbedding, viaFintypeEmbedding_apply_image, castLEEmb_toEmbedding, Function.Embedding.coeFn_mk, coe_castLE,
  coe_finRotate]
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ (if { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } = last ↑i then 0
    else ↑{ val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } + 1) =
    ↑(if castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } = i then 0
      else castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) } + 1)
[PROOFSTEP]
simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
[GOAL]
case succ.h
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
⊢ (if ↑j = ↑i then 0 else ↑j + 1) = ↑(if ↑j = ↑i then 0 else j + 1)
[PROOFSTEP]
split_ifs with heq
[GOAL]
case pos
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ↑j = ↑i
⊢ 0 = ↑0
[PROOFSTEP]
rfl
[GOAL]
case neg
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ¬↑j = ↑i
⊢ ↑j + 1 = ↑(j + 1)
[PROOFSTEP]
rw [Fin.val_add_one_of_lt]
[GOAL]
case neg
n✝ : ℕ
i j : Fin (Nat.succ (Nat.succ n✝))
h : j ≤ i
this : j = castLE (_ : Nat.succ ↑i ≤ Nat.succ (Nat.succ n✝)) { val := ↑j, isLt := (_ : ↑j < Nat.succ ↑i) }
heq : ¬↑j = ↑i
⊢ j < last (n✝ + 1)
[PROOFSTEP]
exact lt_of_lt_of_le (lt_of_le_of_ne h (mt (congr_arg _) heq)) (le_last i)
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(↑(cycleRange i) j) = if j = i then 0 else ↑j + 1
[PROOFSTEP]
rw [cycleRange_of_le h]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
⊢ ↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : j = i
⊢ ↑0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
n : ℕ
i j : Fin (Nat.succ n)
h : j ≤ i
h' : ¬j = i
⊢ ↑(j + 1) = ↑j + 1
[PROOFSTEP]
exact
  val_add_one_of_lt
    (calc
      (j : ℕ) < i := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
      _ ≤ n := Nat.lt_succ_iff.mp i.2)
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j < i
⊢ ↑(cycleRange i) j = j + 1
[PROOFSTEP]
rw [cycleRange_of_le h.le, if_neg h.ne]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j < i
⊢ ↑(↑(cycleRange i) j) = ↑j + 1
[PROOFSTEP]
rw [coe_cycleRange_of_le h.le, if_neg h.ne]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
h : j = i
⊢ ↑(cycleRange i) j = 0
[PROOFSTEP]
rw [cycleRange_of_le h.le, if_pos h]
[GOAL]
n : ℕ
i j : Fin (Nat.succ n)
⊢ ↑(cycleRange i) j = if j < i then j + 1 else if j = i then 0 else j
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h₁ : j < i
⊢ ↑(cycleRange i) j = j + 1
[PROOFSTEP]
exact cycleRange_of_lt h₁
[GOAL]
case pos
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : j = i
⊢ ↑(cycleRange i) j = 0
[PROOFSTEP]
exact cycleRange_of_eq h₂
[GOAL]
case neg
n : ℕ
i j : Fin (Nat.succ n)
h₁ : ¬j < i
h₂ : ¬j = i
⊢ ↑(cycleRange i) j = j
[PROOFSTEP]
exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))
[GOAL]
n : ℕ
⊢ cycleRange 0 = 1
[PROOFSTEP]
ext j
[GOAL]
case H.h
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) j) = ↑(↑1 j)
[PROOFSTEP]
refine' Fin.cases _ (fun j => _) j
[GOAL]
case H.h.refine'_1
n : ℕ
j : Fin (Nat.succ n)
⊢ ↑(↑(cycleRange 0) 0) = ↑(↑1 0)
[PROOFSTEP]
simp
[GOAL]
case H.h.refine'_2
n : ℕ
j✝ : Fin (Nat.succ n)
j : Fin n
⊢ ↑(↑(cycleRange 0) (succ j)) = ↑(↑1 (succ j))
[PROOFSTEP]
rw [cycleRange_of_gt (Fin.succ_pos j), one_apply]
[GOAL]
n : ℕ
⊢ cycleRange (last n) = finRotate (n + 1)
[PROOFSTEP]
ext i
[GOAL]
case H.h
n : ℕ
i : Fin (n + 1)
⊢ ↑(↑(cycleRange (last n)) i) = ↑(↑(finRotate (n + 1)) i)
[PROOFSTEP]
rw [coe_cycleRange_of_le (le_last _), coe_finRotate]
[GOAL]
n : ℕ
h : 0 < n
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
h : 0 < Nat.zero
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
cases h
[GOAL]
case succ
n : ℕ
h : 0 < Nat.succ n
⊢ cycleRange { val := 0, isLt := h } = 1
[PROOFSTEP]
exact cycleRange_zero n
[GOAL]
n : ℕ
i : Fin n
⊢ ↑sign (cycleRange i) = (-1) ^ ↑i
[PROOFSTEP]
simp [cycleRange]
[GOAL]
n : ℕ
i j : Fin n
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
cases n
[GOAL]
case zero
i j : Fin Nat.zero
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rcases j with ⟨_, ⟨⟩⟩
[GOAL]
case succ
n✝ : ℕ
i j : Fin (Nat.succ n✝)
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rcases lt_trichotomy j i with (hlt | heq | hgt)
[GOAL]
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
have : castSucc (j + 1) = j.succ := by
  ext
  rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
[GOAL]
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ castSucc (j + 1) = succ j
[PROOFSTEP]
ext
[GOAL]
case h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
⊢ ↑(castSucc (j + 1)) = ↑(succ j)
[PROOFSTEP]
rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
[GOAL]
case succ.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_below, this, swap_apply_of_ne_of_ne]
[GOAL]
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succ j ≠ 0
[PROOFSTEP]
apply Fin.succ_ne_zero
[GOAL]
case succ.inl.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ succ j ≠ succ i
[PROOFSTEP]
exact (Fin.succ_injective _).ne hlt.ne
[GOAL]
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ castSucc (j + 1) < succ i
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val]
[GOAL]
case succ.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hlt : j < i
this : castSucc (j + 1) = succ j
⊢ ↑(castSucc (j + 1)) < ↑(succ i)
[PROOFSTEP]
simpa [this] using hlt
[GOAL]
case succ.inr.inl
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [heq, Fin.cycleRange_self, Fin.succAbove_below, swap_apply_right, Fin.castSucc_zero]
[GOAL]
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ castSucc 0 < succ i
[PROOFSTEP]
rw [Fin.castSucc_zero]
[GOAL]
case succ.inr.inl.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
heq : j = i
⊢ 0 < succ i
[PROOFSTEP]
apply Fin.succ_pos
[GOAL]
case succ.inr.inr
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succAbove (succ i) (↑(cycleRange i) j) = ↑(swap 0 (succ i)) (succ j)
[PROOFSTEP]
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_above, swap_apply_of_ne_of_ne]
[GOAL]
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ 0
[PROOFSTEP]
apply Fin.succ_ne_zero
[GOAL]
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ j ≠ succ i
[PROOFSTEP]
apply (Fin.succ_injective _).ne hgt.ne.symm
[GOAL]
case succ.inr.inr.h
n✝ : ℕ
i j : Fin (Nat.succ n✝)
hgt : i < j
⊢ succ i ≤ castSucc j
[PROOFSTEP]
simpa [Fin.le_iff_val_le_val] using hgt
[GOAL]
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
cases' lt_or_ge (castSucc j) i with h h
[GOAL]
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j < i
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
rw [Fin.succAbove_below _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
[GOAL]
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : castSucc j ≥ i
⊢ ↑(cycleRange i) (succAbove i j) = succ j
[PROOFSTEP]
rw [Fin.succAbove_above _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ ↑(cycleRange i) (↑(cycleRange i).symm 0) = ↑(cycleRange i) i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ ↑(cycleRange i) (↑(cycleRange i).symm (succ j)) = ↑(cycleRange i) (succAbove i j)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ IsCycle (cycleRange i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := i, isLt := hi })
[PROOFSTEP]
cases i
[GOAL]
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.zero, isLt := hi })
[PROOFSTEP]
exact (h0 rfl).elim
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ IsCycle (cycleRange { val := Nat.succ n✝, isLt := hi })
[PROOFSTEP]
exact isCycle_finRotate.extendDomain _
[GOAL]
n : ℕ
i : Fin (n + 1)
h0 : i ≠ 0
⊢ cycleType (cycleRange i) = {↑i + 1}
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
n i : ℕ
hi : i < n + 1
h0 : { val := i, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := i, isLt := hi }) = {↑{ val := i, isLt := hi } + 1}
[PROOFSTEP]
cases i
[GOAL]
case mk.zero
n : ℕ
hi : Nat.zero < n + 1
h0 : { val := Nat.zero, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := Nat.zero, isLt := hi }) = {↑{ val := Nat.zero, isLt := hi } + 1}
[PROOFSTEP]
exact (h0 rfl).elim
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ cycleType (cycleRange { val := Nat.succ n✝, isLt := hi }) = {↑{ val := Nat.succ n✝, isLt := hi } + 1}
[PROOFSTEP]
rw [cycleRange, cycleType_extendDomain]
[GOAL]
case mk.succ
n n✝ : ℕ
hi : Nat.succ n✝ < n + 1
h0 : { val := Nat.succ n✝, isLt := hi } ≠ 0
⊢ cycleType (finRotate (↑{ val := Nat.succ n✝, isLt := hi } + 1)) = {↑{ val := Nat.succ n✝, isLt := hi } + 1}
[PROOFSTEP]
exact cycleType_finRotate
[GOAL]
n : ℕ
⊢ IsThreeCycle (cycleRange 2)
[PROOFSTEP]
rw [IsThreeCycle, cycleType_cycleRange]
[GOAL]
n : ℕ
⊢ {↑2 + 1} = {3}
[PROOFSTEP]
simp [Fin.eq_iff_veq]
[GOAL]
n : ℕ
⊢ 2 ≠ 0
[PROOFSTEP]
simp [Fin.eq_iff_veq]


[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
S : Submonoid M
hs : s ⊆ ↑S
ht : t ⊆ ↑S
⊢ s * t ⊆ ↑S
[PROOFSTEP]
rintro _ ⟨p, q, hp, hq, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
S : Submonoid M
hs : s ⊆ ↑S
ht : t ⊆ ↑S
p q : M
hp : p ∈ s
hq : q ∈ t
⊢ (fun x x_1 => x * x_1) p q ∈ ↑S
[PROOFSTEP]
exact Submonoid.mul_mem _ (hs hp) (ht hq)
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
⊢ ↑s * ↑s = ↑s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s ↔ x ∈ ↑s
[PROOFSTEP]
refine' ⟨_, fun h => ⟨x, 1, h, s.one_mem, mul_one x⟩⟩
[GOAL]
case h
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s → x ∈ ↑s
[PROOFSTEP]
rintro ⟨a, b, ha, hb, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
a b : M
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ (fun x x_1 => x * x_1) a b ∈ ↑s
[PROOFSTEP]
exact s.mul_mem ha hb
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K
[PROOFSTEP]
rw [closure_eq, closure_eq]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)
[PROOFSTEP]
refine' @closure_induction N _ s (fun x : N => ∃ n : ℕ, r ^ n • x ∈ closure (r • s)) _ hx _ _ _
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x : N), x ∈ s → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x : N
hx : x ∈ s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)
[PROOFSTEP]
exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x : N
hx : x ∈ s
⊢ (fun x => r • x) x = r ^ 1 • x
[PROOFSTEP]
rw [pow_one]
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) 1
[PROOFSTEP]
exact ⟨0, by simpa using one_mem _⟩
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ r ^ 0 • 1 ∈ closure (r • s)
[PROOFSTEP]
simpa using one_mem _
[GOAL]
case refine'_3
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x y : N),
    (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x →
      (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) y → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) (x * y)
[PROOFSTEP]
rintro x y ⟨nx, hx⟩ ⟨ny, hy⟩
[GOAL]
case refine'_3.intro.intro
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)
[PROOFSTEP]
use ny + nx
[GOAL]
case h
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ (ny + nx) • (x * y) ∈ closure (r • s)
[PROOFSTEP]
rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
[GOAL]
case h
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_6
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • y * r ^ nx • x ∈ closure (r • s)
[PROOFSTEP]
exact mul_mem hy hx
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ a✝ * b✝ ∈ (↑S)⁻¹
[PROOFSTEP]
rw [mem_inv, mul_inv_rev]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S
[PROOFSTEP]
exact mul_mem hb ha
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ ↑S
[PROOFSTEP]
rw [inv_one]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1 ∈ ↑S
[PROOFSTEP]
exact S.one_mem'
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹
[PROOFSTEP]
rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)
[PROOFSTEP]
exact subset_closure
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹
[PROOFSTEP]
rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s✝ t u : Set M
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)
[PROOFSTEP]
exact subset_closure
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ 1 • S = S
[PROOFSTEP]
change S.map _ = S
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ map (↑(MulDistribMulAction.toMonoidEnd α M) 1) S = S
[PROOFSTEP]
simpa only [map_one] using S.map_id
[GOAL]
α : Type u_1
G✝ : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
G : Type u_6
inst✝ : Group G
S : Set G
x : G
⊢ x ∈ closure S⁻¹ ↔ x⁻¹ ∈ closure S
[PROOFSTEP]
rw [closure_inv, mem_inv]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ 1 = closure {1}
[PROOFSTEP]
rw [closure_singleton_eq, one_eq_mrange]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange (↑(multiplesHom R) 1)
[PROOFSTEP]
congr 1
[GOAL]
case e_f
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ Nat.castAddMonoidHom R = ↑(multiplesHom R) 1
[PROOFSTEP]
ext
[GOAL]
case e_f.a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : AddMonoidWithOne R
⊢ ↑(Nat.castAddMonoidHom R) 1 = ↑(↑(multiplesHom R) 1) 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
m n : R
hm : m ∈ M
hn : n ∈ N
⊢ ↑(↑AddMonoidHom.mul ↑{ val := m, property := hm }) n = m * n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
C : R → Prop
r : R
hr : r ∈ M * N
hm : ∀ (m : R), m ∈ M → ∀ (n : R), n ∈ N → C (m * n)
ha : ∀ (x y : R), C x → C y → C (x + y)
⊢ 0 ∈ { carrier := setOf C, add_mem' := (_ : ∀ {a b : R}, C a → C b → C (a + b)) }.carrier
[PROOFSTEP]
simpa only [zero_mul] using hm _ (zero_mem _) _ (zero_mem _)
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T = closure (S * T)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)
[PROOFSTEP]
refine mul_le.2 fun a ha b hb => ?_
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a * b ∈ closure (S * T)
[PROOFSTEP]
rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a ∈ comap (AddMonoidHom.mulRight b) (closure (S * T))
[PROOFSTEP]
refine (closure_le.2 fun a' ha' => ?_) ha
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ a' ∈ ↑(comap (AddMonoidHom.mulRight b) (closure (S * T)))
[PROOFSTEP]
change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
⊢ b ∈ comap (AddMonoidHom.mulLeft a') (closure (S * T))
[PROOFSTEP]
refine (closure_le.2 fun b' hb' => ?_) hb
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ b' ∈ ↑(comap (AddMonoidHom.mulLeft a') (closure (S * T)))
[PROOFSTEP]
change a' * b' ∈ closure (S * T)
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
a' : R
ha' : a' ∈ S
b' : R
hb' : b' ∈ T
⊢ a' * b' ∈ closure (S * T)
[PROOFSTEP]
exact subset_closure (Set.mul_mem_mul ha' hb')
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T
[PROOFSTEP]
rw [closure_le]
[GOAL]
case a
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)
[PROOFSTEP]
rintro _ ⟨a, b, ha, hb, rfl⟩
[GOAL]
case a.intro.intro.intro.intro
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a b : R
ha : a ∈ S
hb : b ∈ T
⊢ (fun x x_1 => x * x_1) a b ∈ ↑(closure S * closure T)
[PROOFSTEP]
exact mul_mem_mul (subset_closure ha) (subset_closure hb)
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure (↑M * ↑N)
[PROOFSTEP]
rw [← closure_mul_closure, closure_eq, closure_eq]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : R
hn : n ∈ ⊥
⊢ m * n ∈ ⊥
[PROOFSTEP]
rw [AddSubmonoid.mem_bot] at hn ⊢
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : R
hn : n = 0
⊢ m * n = 0
[PROOFSTEP]
rw [hn, mul_zero]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m ∈ ⊥
n : R
hn : n ∈ S
⊢ m * n ∈ ⊥
[PROOFSTEP]
rw [AddSubmonoid.mem_bot] at hm ⊢
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
hn : n ∈ S
⊢ m * n = 0
[PROOFSTEP]
rw [hm, zero_mul]
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ ↑M * ↑N ⊆ ↑(M * N)
[PROOFSTEP]
rintro _ ⟨i, j, hi, hj, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
i j : R
hi : i ∈ ↑M
hj : j ∈ ↑N
⊢ (fun x x_1 => x * x_1) i j ∈ ↑(M * N)
[PROOFSTEP]
exact mul_mem_mul hi hj
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
⊢ -x * y = -(x * y)
[PROOFSTEP]
refine' le_antisymm (mul_le.2 fun m hm n hn => _) ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => _)
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ -x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * y)
[PROOFSTEP]
simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(-x * y)
[PROOFSTEP]
simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m n : R
hn : n ∈ y
hm : -m ∈ x
⊢ -m * n ∈ x * y
[PROOFSTEP]
exact mul_mem_mul hm hn
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y
[PROOFSTEP]
exact mul_mem_mul (neg_mem_neg.2 hm) hn
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
⊢ x * -y = -(x * y)
[PROOFSTEP]
refine' le_antisymm (mul_le.2 fun m hm n hn => _) ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => _)
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ -y
⊢ m * n ∈ -(x * y)
[PROOFSTEP]
simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * n ∈ -(x * -y)
[PROOFSTEP]
simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : -n ∈ y
⊢ m * -n ∈ x * y
[PROOFSTEP]
exact mul_mem_mul hm hn
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocRing R
src✝ : InvolutiveNeg (AddSubmonoid R) := involutiveNeg
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ m * -n ∈ x * -y
[PROOFSTEP]
exact mul_mem_mul hm (neg_mem_neg.2 hn)
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ 1 * M = M
[PROOFSTEP]
rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
[GOAL]
α : Type u_1
G : Type u_2
M✝ : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ M * 1 = M
[PROOFSTEP]
rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : Set R
⊢ closure s ^ 0 = closure (s ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero, one_eq_closure_one_set]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure s ^ (n + 1) = closure (s ^ (n + 1))
[PROOFSTEP]
rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = closure (↑s ^ n)
[PROOFSTEP]
rw [← closure_pow, closure_eq]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ IsPwo ↑(Submonoid.closure s)
[PROOFSTEP]
rw [Submonoid.closure_eq_image_prod]
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ IsPwo (List.prod '' {l | ∀ (x : α), x ∈ l → x ∈ s})
[PROOFSTEP]
refine' (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on _
[GOAL]
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ ∀ (a₁ : List α),
    a₁ ∈ {l | ∀ (x : α), x ∈ l → x ∈ s} →
      ∀ (a₂ : List α),
        a₂ ∈ {l | ∀ (x : α), x ∈ l → x ∈ s} →
          List.SublistForall₂ (fun x x_1 => x ≤ x_1) a₁ a₂ → List.prod a₁ ≤ List.prod a₂
[PROOFSTEP]
exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx


[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
⊢ zpowers g = closure {g}
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
[PROOFSTEP]
exact mem_closure_singleton.symm
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
N : Type u_3
inst✝¹ : Group N
R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r
[PROOFSTEP]
simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
N : Type u_3
inst✝¹ : Group N
R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ (fun x => x • 1) k = ↑k
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝³ : Group G
A✝ : Type u_2
inst✝² : AddGroup A✝
N : Type u_3
inst✝¹ : Group N
A : Type u_4
inst✝ : AddGroupWithOne A
⊢ AddMonoidHom.range (castAddHom A) = AddSubgroup.zmultiples 1
[PROOFSTEP]
ext a
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
A✝ : Type u_2
inst✝² : AddGroup A✝
N : Type u_3
inst✝¹ : Group N
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ AddMonoidHom.range (castAddHom A) ↔ a ∈ AddSubgroup.zmultiples 1
[PROOFSTEP]
simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (↑f x)
[PROOFSTEP]
rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
a b k : ℤ
⊢ (fun x => x • a) k = b ↔ b = a * k
[PROOFSTEP]
rw [mul_comm, eq_comm, ← smul_eq_mul]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
⊢ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
ext y
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x) → y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
rintro ⟨z, ⟨m, hm⟩, hz2⟩
[GOAL]
case h.mp.intro.intro.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : (fun x x_1 => x ^ x_1) x m = z
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x))
[PROOFSTEP]
use m
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : (fun x x_1 => x ^ x_1) x m = z
⊢ (fun x_1 => x_1 • ↑Additive.ofMul x) m = y
[PROOFSTEP]
simp only at *
[GOAL]
case h
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
z : G
hz2 : ↑Additive.ofMul z = y
m : ℤ
hm : x ^ m = z
⊢ m • ↑Additive.ofMul x = y
[PROOFSTEP]
rwa [← ofMul_zpow, hm]
[GOAL]
case h.mpr
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
⊢ y ∈ ↑(AddSubgroup.zmultiples (↑Additive.ofMul x)) → y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • ↑Additive.ofMul x) n = y
⊢ y ∈ ↑Additive.ofMul '' ↑(Subgroup.zpowers x)
[PROOFSTEP]
refine' ⟨x ^ n, ⟨n, rfl⟩, _⟩
[GOAL]
case h.mpr.intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : G
y : Additive G
n : ℤ
hn : (fun x_1 => x_1 • ↑Additive.ofMul x) n = y
⊢ ↑Additive.ofMul (x ^ n) = y
[PROOFSTEP]
rwa [ofMul_zpow]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x))
[PROOFSTEP]
symm
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x)) = ↑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)
[PROOFSTEP]
rw [Equiv.eq_image_iff_symm_image_eq]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
x : A
⊢ ↑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (↑Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)
[PROOFSTEP]
exact ofMul_image_zpowers_eq_zmultiples_ofMul
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
x✝¹ x✝ : { x // x ∈ zpowers g }
val✝¹ : G
w✝¹ : ℤ
h₁ : (fun x x_1 => x ^ x_1) g w✝¹ = val✝¹
val✝ : G
w✝ : ℤ
h₂ : (fun x x_1 => x ^ x_1) g w✝ = val✝
⊢ { val := val✝¹, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝¹) } *
      { val := val✝, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝) } =
    { val := val✝, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝) } *
      { val := val✝¹, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) g y = val✝¹) }
[PROOFSTEP]
rw [Subtype.ext_iff, coe_mul, coe_mul, Subtype.coe_mk, Subtype.coe_mk, ← h₁, ← h₂, zpow_mul_comm]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H
[PROOFSTEP]
rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g✝ g : G
⊢ zpowers g = ⊥ ↔ g = 1
[PROOFSTEP]
rw [eq_bot_iff, zpowers_le, mem_bot]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : G) (_ : g ∈ S), centralizer ↑(zpowers g)
[PROOFSTEP]
rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
s : Set G
g : G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ (g : ↑S), centralizer ↑(zpowers ↑g)
[PROOFSTEP]
rw [center_eq_iInf S hS, ← iInf_subtype'']