invoke

Stream: mathlib4

[vxctyxeha]

how to invoke c1 at n+2

import Mathlib
open Nat
open Equiv Subgroup

theorem c1 (n : ℕ) : Subgroup.closure {finRotate (n + 2), swap 0 1} = ⊤ := by
  have swapeq : swap 0 1 = swap 0 (finRotate (n + 2) 0) := by
    simp only [finRotate_succ_apply, zero_add]
  rw [swapeq]
  apply Perm.closure_cycle_adjacent_swap
  ·
    show (finRotate (n + 2)).IsCycle
    exact isCycle_finRotate
  ·
    show (finRotate (n + 2)).support = Finset.univ
    exact support_finRotate
theorem c2 (n : ℕ)[NeZero n] (hn : 2 ≤ n) : Subgroup.closure {finRotate n , swap 0 1} = ⊤ := by

[Eric Wieser]

Please try to come up with better titles

[Eric Wieser]

docs#exists_add_of_le probably helps

[vxctyxeha]

tactic 'rewrite' failed, motive is not type correct:
fun _a => Subgroup.closure {finRotate _a, swap 0 1} = ⊤
Error: application type mismatch
@Fin.instOfNat _a ⋯
argument
inst✝
has type
NeZero m : Prop
but is expected to have type
NeZero _a : Prop

import Mathlib
open Nat
open Equiv Subgroup


theorem c1 (n : ℕ) : Subgroup.closure {finRotate (n + 2), swap 0 1} = ⊤ := by
  have swapeq : swap 0 1 = swap 0 (finRotate (n + 2) 0) := by
    simp only [finRotate_succ_apply, zero_add]
  rw [swapeq]
  apply Perm.closure_cycle_adjacent_swap
  ·
    show (finRotate (n + 2)).IsCycle
    exact isCycle_finRotate
  ·
    show (finRotate (n + 2)).support = Finset.univ
    exact support_finRotate
theorem c2 (m : ℕ)[NeZero m] (hn : 2 ≤ m) : Subgroup.closure {finRotate m , swap 0 1} = ⊤ := by

  let k := m - 2
  have h_k : m =k+2 := by
    exact (Nat.sub_eq_iff_eq_add hn).mp rfl
  rw [h_k]

[Robin Arnez]

Here:

import Mathlib.GroupTheory.Perm.Fin

theorem c1 (n : ℕ) : Subgroup.closure {finRotate (n + 2), Equiv.swap 0 1} = ⊤ := by
  have swapeq : Equiv.swap 0 1 = Equiv.swap 0 (finRotate (n + 2) 0) := by
    simp only [finRotate_succ_apply, zero_add]
  rw [swapeq]
  apply Equiv.Perm.closure_cycle_adjacent_swap
  · show (finRotate (n + 2)).IsCycle
    exact isCycle_finRotate
  · show (finRotate (n + 2)).support = Finset.univ
    exact support_finRotate

theorem c2 (m : ℕ) [h : NeZero m] (hn : 2 ≤ m) : Subgroup.closure {finRotate m, Equiv.swap 0 1} = ⊤ := by
  obtain ⟨_, rfl⟩ := Nat.exists_eq_add_of_le' hn
  apply c1

using Nat.exists_eq_add_of_le'