awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
⊢ (finSumNatEquiv n : (a : Fin n ⊕ ℕ) → ℕ) (Sum.inr i) = n + i

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
hi : i < n
⊢ Eq (α := Fin n ⊕ ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i : Fin n ⊕ ℕ) (Sum.inl ⟨i, hi⟩ : Fin n ⊕ ℕ)

Tactic:
dif_pos hi

Premises used: dif_pos, dite
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
hi : n ≤ i
⊢ Eq (α := Fin n ⊕ ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i : Fin n ⊕ ℕ) (Sum.inr (i - n) : Fin n ⊕ ℕ)

Tactic:
dif_neg (Nat.not_lt_of_ge hi)

Premises used: dif_neg, dite, Nat.not_lt_of_ge
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ Eq (α := Fin n ⊕ ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) (↑i : ℕ) : Fin n ⊕ ℕ) (Sum.inl i : Fin n ⊕ ℕ)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
⊢ Eq (α := Fin n ⊕ ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) (i + n) : Fin n ⊕ ℕ) (Sum.inr i : Fin n ⊕ ℕ)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
⊢ Eq (α := Fin n ⊕ ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) (n + i) : Fin n ⊕ ℕ) (Sum.inr i : Fin n ⊕ ℕ)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
inl :
  ∀ (hi : i < n), Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
inr :
  ∀ (hi : i ≥ n), Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)

Tactic:
rcases i.lt_or_ge n with hi | hi

Premises used: Nat.lt_or_ge
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
hi : i < n
inl : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide (i < n)
inl₁ : Sum.isLeft (β := ℕ) (Sum.inl (⟨i, hi⟩ : Fin n)) = decide True
inl₂ : true = decide True
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)

Tactic:
simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]

Premises used: decide_true, finSumNatEquiv_symm_apply_of_lt, Sum.isLeft_inl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
hi : i ≥ n
inr : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide (i < n)
inr₁ : Sum.isLeft (α := Fin n) (Sum.inr (i - n)) = decide False
inr₂ : false = decide False
⊢ Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (i < n)

Tactic:
simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]

Premises used: Sum.isLeft_inr, decide_false, LE.le.not_gt, finSumNatEquiv_symm_apply_of_ge
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
simp_rw :
  Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) =
    !Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i)
⊢ Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) = decide (n ≤ i)

Tactic:
simp_rw [← not_lt, decide_not, ← isLeft_finSumNatEquiv_symm_apply]

Premises used: decide_not, isLeft_finSumNatEquiv_symm_apply, not_lt
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
inl : ∀ (val : Fin n), Sum.isRight (β := ℕ) (Sum.inl val) = !Sum.isLeft (β := ℕ) (Sum.inl val)
inr : ∀ (val : ℕ), Sum.isRight (α := Fin n) (Sum.inr val) = !Sum.isLeft (α := Fin n) (Sum.inr val)
⊢ Sum.isRight (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i) =
    !Sum.isLeft (α := Fin n) (β := ℕ) (((finSumNatEquiv n).symm : (a : ℕ) → Fin n ⊕ ℕ) i)

Tactic:
cases (finSumNatEquiv n).symm i

Premises used: finSumNatEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i : ℕ
val : Fin n
⊢ Sum.isRight (β := ℕ) (Sum.inl val) = !Sum.isLeft (β := ℕ) (Sum.inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n i val : ℕ
⊢ Sum.isRight (α := Fin n) (Sum.inr val) = !Sum.isLeft (α := Fin n) (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m : ℕ
k : Fin m
n : ℕ
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) (Fin.castAdd n k) = Fin.natAdd n k

Tactic:
simp [finAddFlip]

Premises used: finAddFlip
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
n : ℕ
k : Fin n
m : ℕ
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) (Fin.natAdd m k) = Fin.castAdd m k

Tactic:
simp [finAddFlip]

Premises used: finAddFlip
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h : k < m
hk : k < m + n
hnk : n + k < n + m
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) (Fin.castAdd n ⟨k, h⟩) = Fin.natAdd n (⟨k, h⟩ : Fin m)

Tactic:
finAddFlip_apply_castAdd ⟨k, h⟩ n

Premises used: Fin.mk, finAddFlip_apply_castAdd
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h : k < m
hk : k < m + n
hnk : n + k < n + m
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) ⟨k, hk⟩ = (⟨n + k, hnk⟩ : Fin (n + m))

Tactic:
convert! finAddFlip_apply_castAdd ⟨k, h⟩ n

Premises used: Fin.mk, finAddFlip_apply_castAdd
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n + m

Tactic:
lia
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n

Tactic:
lia
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
h : k = (↑(Fin.natAdd m (⟨k - m, ⋯⟩ : Fin n)) : ℕ)
⊢ (finAddFlip : (a : Fin (m + n)) → Fin (n + m)) ⟨k, h₂⟩ = (⟨k - m, ⋯⟩ : Fin (n + m))

Tactic:
convert! @finAddFlip_apply_natAdd n ⟨k - m, by lia⟩ m

Premises used: HSub.hSub, Fin.mk, finAddFlip_apply_natAdd
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = (↑(Fin.natAdd m (⟨k - m, ⋯⟩ : Fin n)) : ℕ)

Tactic:
simp [Nat.add_sub_cancel' h₁]

Premises used: Nat.add_sub_cancel'
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x : Fin m × Fin n
⊢ (↑x.2 : ℕ) + n * (↑x.1 : ℕ) + 1 = (↑x.1 : ℕ) * n + (↑x.2 : ℕ) + 1

Tactic:
ac_rfl
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n : ℕ
x_1 : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
rw rw₁ : 0 + (↑x : ℕ) = 0 + (↑x : ℕ)
⊢ (↑y : ℕ) / n + (↑x : ℕ) = 0 + (↑x : ℕ)

Tactic:
rw [Nat.div_eq_of_lt y.2]

Premises used: Fin.isLt, Nat.div_eq_of_lt
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
⊢ (fun (a : ℕ) ↦ (a / n, Fin.ofNat n a)) ((fun (p : ℕ × Fin n) ↦ p.1 * n + (↑p.2 : ℕ)) p) = p

Tactic:
Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)

Premises used: Fin.is_lt, Fin.ext, Nat.mul_add_mod_of_lt, Prod.ext, Prod.snd
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
refine : ((fun (a : ℕ) ↦ (a / n, Fin.ofNat n a)) ((fun (p : ℕ × Fin n) ↦ p.1 * n + (↑p.2 : ℕ)) p)).1 = p.1
⊢ (fun (a : ℕ) ↦ (a / n, Fin.ofNat n a)) ((fun (p : ℕ × Fin n) ↦ p.1 * n + (↑p.2 : ℕ)) p) = p

Tactic:
refine Prod.ext ?_ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)

Premises used: Fin.ext, Prod.ext
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
p : ℕ × Fin n
rw : ((↑p.2 : ℕ) + p.1 * n) / n = p.1
rw₁ : (↑p.2 : ℕ) / n + p.1 = p.1
rw₂ : 0 + p.1 = p.1
rw₃ rw₄ : p.1 = p.1
⊢ (p.1 * n + (↑p.2 : ℕ)) / n = p.1

Tactic:
rw [Nat.add_comm, Nat.add_mul_div_right _ _ n.pos_of_neZero, Nat.div_eq_of_lt p.2.is_lt,
      Nat.zero_add]

Premises used: Fin.is_lt, Nat.add_mul_div_right, Nat.pos_of_neZero, Nat.div_eq_of_lt, Nat.zero_add, Prod.snd, Nat.add_comm
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
a : ℤ
simp_rw simp_rw₁ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(↑(Fin.ofNat n (a.natMod (↑n : ℤ))) : ℕ) : ℤ) = a
simp_rw₂ : a / (↑n : ℤ) * (↑n : ℤ) + (↑(a.natMod (↑n : ℤ) % n) : ℤ) = a
simp_rw₃ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a.natMod (↑n : ℤ)) : ℤ) (↑n : ℤ) = a
simp_rw₄ : a / (↑n : ℤ) * (↑n : ℤ) + HMod.hMod (α := ℤ) (↑(a % (↑n : ℤ)).toNat : ℤ) (↑n : ℤ) = a
simp_rw₅ : a / (↑n : ℤ) * (↑n : ℤ) + a % (↑n : ℤ) % (↑n : ℤ) = a
simp_rw₆ : a / (↑n : ℤ) * (↑n : ℤ) + a % (↑n : ℤ) = a
⊢ (fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ))
      ((fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ)))) a) =
    a

Tactic:
simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]

Premises used: Iff.mpr, Int.toNat_of_nonneg, Iff.not, Int.natCast_eq_zero, Int.ediv_mul_add_emod, Int.emod_emod, Int.natCast_mod, Int.emod_nonneg, Int.natMod, NeZero.ne, Fin.val_ofNat
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
simp : (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r
⊢ (fun (a : ℤ) ↦ (a / (↑n : ℤ), Fin.ofNat n (a.natMod (↑n : ℤ))))
      ((fun (p : ℤ × Fin n) ↦ p.1 * (↑n : ℤ) + (↑(↑p.2 : ℕ) : ℤ)) (q, ⟨r, hrn⟩)) =
    (q, (⟨r, hrn⟩ : Fin n))

Tactic:
simp only [Prod.mk_inj, Fin.ext_iff]

Premises used: Fin.ext_iff, Prod.mk_inj
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ LE.le (α := ℤ) 0 (↑r : ℤ)

Tactic:
obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn

Premises used: Iff.mpr, Int.ofNat_lt, Int.natCast_nonneg
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
⊢ LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)

Tactic:
obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn

Premises used: Iff.mpr, Int.ofNat_lt, Int.natCast_nonneg
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
h2 : LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)
rw : 0 + q = q ∧ (↑(Fin.ofNat n r) : ℕ) = r
⊢ (q * (↑n : ℤ) + (↑r : ℤ)) / (↑n : ℤ) = q ∧ (↑(Fin.ofNat n ((q * (↑n : ℤ) + (↑r : ℤ)).natMod (↑n : ℤ))) : ℕ) = r

Tactic:
rw [Int.add_comm, add_mul_ediv_right _ _ (natCast_eq_zero.not.2 (NeZero.ne n)),
      ediv_eq_zero_of_lt h1 h2, natMod, add_mul_emod_self_right, emod_eq_of_lt h1 h2, toNat_natCast]

Premises used: Iff.mpr, Int.toNat_natCast, Int.emod_eq_of_lt, Iff.not, Int.natCast_eq_zero, Int.add_comm, Int.ediv_eq_zero_of_lt, Int.add_mul_emod_self_right, Int.add_mul_ediv_right, Int.natMod, NeZero.ne
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
h2 : LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)
⊢ 0 + q = q ∧ (↑(Fin.ofNat n r) : ℕ) = r

Tactic:
⟨q.zero_add, Fin.val_cast_of_lt hrn⟩

Premises used: And.intro, Fin.val_cast_of_lt, Int.zero_add
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m n_1 n : ℕ
inst : NeZero n
x : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : LE.le (α := ℤ) 0 (↑r : ℤ)
h2 : LT.lt (α := ℤ) (↑r : ℤ) (↑n : ℤ)
⊢ 0 + q = q ∧ (↑(Fin.ofNat n r) : ℕ) = r

Tactic:
exact ⟨q.zero_add, Fin.val_cast_of_lt hrn⟩
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m_1 n_1 n m : ℕ
h : n ≤ m
i : Fin n
⊢ (↑(castLE h i) : ℕ) < n

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m_1 n_1 n m : ℕ
h : n ≤ m
x : Fin n
⊢ (fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ (⟨(↑(↑i : Fin m) : ℕ), ⋯⟩ : Fin n))
      ((fun (i : Fin n) ↦
          (Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯ : { i : Fin m // (↑i : ℕ) < n }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m_1 n_1 n m : ℕ
h : n ≤ m
x : { i : Fin m // (↑i : ℕ) < n }
⊢ (fun (i : Fin n) ↦ (Subtype.mk (p := fun (i : Fin m) ↦ (↑i : ℕ) < n) (castLE h i) ⋯ : { i : Fin m // (↑i : ℕ) < n }))
      ((fun (i : { i : Fin m // (↑i : ℕ) < n }) ↦ (⟨(↑(↑i : Fin m) : ℕ), ⋯⟩ : Fin n)) x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m_1 n_1 : ℕ
α : Type u_1
m n : ℕ
fg : (Fin m → α) × (Fin n → α)
⊢ (fun (f : Fin (m + n) → α) ↦
        ((fun (i : Fin m) ↦ f (castAdd n i), fun (i : Fin n) ↦ f (natAdd m i)) : (Fin m → α) × (Fin n → α)))
      ((fun (fg : (Fin m → α) × (Fin n → α)) ↦ append fg.1 fg.2) fg) =
    fg

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Basic
Goal:
m_1 n_1 : ℕ
α : Type u_1
m n : ℕ
f : Fin (m + n) → α
⊢ (fun (fg : (Fin m → α) × (Fin n → α)) ↦ append fg.1 fg.2)
      ((fun (f : Fin (m + n) → α) ↦
          ((fun (i : Fin m) ↦ f (castAdd n i), fun (i : Fin n) ↦ f (natAdd m i)) : (Fin m → α) × (Fin n → α)))
        f) =
    f

Tactic:
simp [Fin.append_castAdd_natAdd]

Premises used: Fin.append_castAdd_natAdd
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
⊢ Eq (α := Equiv.Perm (Fin 0)) (finRotate 0) (Equiv.refl (Fin 0))

Tactic:
rfl

Premises used: finRotate, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
⊢ Eq (α := Equiv.Perm (Fin (n + 1))) (finRotate (n + 1)) (Equiv.trans finAddFlip (finCongr ⋯))

Tactic:
rfl

Premises used: finRotate, rfl
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n k : ℕ
h : k < n
h₁ :
  (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) (⟨k, ⋯⟩ : Fin (n + 1))) : ℕ) =
    (↑(⟨k + 1, ⋯⟩ : Fin (n + 1)) : ℕ)
⊢ (finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨k, ⋯⟩ = (⟨k + 1, ⋯⟩ : Fin (n + 1))

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n k : ℕ
h : k < n
h₁ : (↑((finAddFlip : (a : Fin (n + 1)) → Fin (1 + n)) (⟨k, ⋯⟩ : Fin (n + 1))) : ℕ) = k + 1
⊢ (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) (⟨k, ⋯⟩ : Fin (n + 1))) : ℕ) =
    (↑(⟨k + 1, ⋯⟩ : Fin (n + 1)) : ℕ)

Tactic:
dsimp [finRotate_succ]

Premises used: finRotate_succ
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n k : ℕ
h : k < n
⊢ (↑((finAddFlip : (a : Fin (n + 1)) → Fin (1 + n)) (⟨k, ⋯⟩ : Fin (n + 1))) : ℕ) = k + 1

Tactic:
simp [finAddFlip_apply_mk_left h, Nat.add_comm]

Premises used: finAddFlip_apply_mk_left, Nat.add_lt_add_left, Nat.lt_add_right, Nat.add_comm
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
⊢ n < n + 1

Tactic:
lia
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
rw : Fin.cast ⋯ (⟨n - n, ⋯⟩ : Fin (1 + n)) = 0
⊢ Eq (α := Fin (n + 1)) (Fin.cast ⋯ ((finAddFlip : (a : Fin (n + 1)) → Fin (1 + n)) ⟨n, ⋯⟩)) 0

Tactic:
rw [finAddFlip_apply_mk_right le_rfl]

Premises used: le_rfl, finAddFlip_apply_mk_right
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
⊢ Fin.cast ⋯ (⟨n - n, ⋯⟩ : Fin (1 + n)) = 0

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.last n) : Fin (n + 1))
    (0 : Fin (n + 1))

Tactic:
finRotate_last'

Premises used: Fin.ofNat, finRotate_last', Nat.mod
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h :
  ∀ (i : ℕ) (h : i < n + 1),
    Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
      (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) → α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a) fun (i : Fin (n + 1)) ↦
    cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)

Tactic:
ext ⟨i, h⟩
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
pos :
  ∀ (h' : i < n),
    Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
      (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
neg :
  ∀ (h' : ¬i < n),
    Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
      (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)

Tactic:
by_cases h' : i < n
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
pos :
  Eq.{u_1 + 1} (α := α) (cast ⋯ (v ((⟨i, h⟩ : Fin (n + 1)).castLT h')) : α)
    (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨i + 1, ⋯⟩ : Fin (n + 1)) : α)
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)

Tactic:
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']

Premises used: Fin.cons, finRotate_of_lt, dif_pos, Fin.snoc
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ Eq.{u_1 + 1} (α := α) (cast ⋯ (v ((⟨i, h⟩ : Fin (n + 1)).castLT h')) : α)
    (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨i + 1, ⋯⟩ : Fin (n + 1)) : α)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n ≤ i

Tactic:
simp only [not_lt] at h'

Premises used: not_lt
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i

Tactic:
(Nat.eq_of_le_of_lt_succ h' h).symm

Premises used: Nat.eq_of_le_of_lt_succ, Eq.symm
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i

Tactic:
exact (Nat.eq_of_le_of_lt_succ h' h).symm

Premises used: Nat.eq_of_le_of_lt_succ, Eq.symm
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i

Tactic:
have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
neg :
  ∀ (h : n < n + 1) (h' : ¬n < n),
    Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨n, h⟩ : Fin (n + 1)) : α)
      (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨n, h⟩) : α)
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨i, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨i, h⟩) : α)

Tactic:
subst h''
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
neg : Eq.{u_1 + 1} (α := α) (cast ⋯ a : α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨0, ⋯⟩ : Fin (n + 1)) : α)
⊢ Eq.{u_1 + 1} (α := α) (snoc (α := fun (x : Fin (n + 1)) ↦ α) v a (⟨n, h⟩ : Fin (n + 1)) : α)
    (cons (α := fun (x : Fin (n + 1)) ↦ α) a v ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) ⟨n, h⟩) : α)

Tactic:
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]

Premises used: lt_irrefl, Fin.cons, Fin.snoc, dif_neg, finRotate_last'
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ Eq.{u_1 + 1} (α := α) (cast ⋯ a : α) (cases (motive := fun (x : Fin (n + 1)) ↦ α) a v (⟨0, ⋯⟩ : Fin (n + 1)) : α)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
⊢ Eq (α := Equiv.Perm (Fin 1)) (finRotate 1) (Equiv.refl (Fin 1))

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin 0
⊢ (finRotate 0 : (a : Fin 0) → Fin 0) i = i + 1

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin 0
⊢ (finRotate 0 : (a : Fin 0) → Fin 0) i = i + 1

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin 1
⊢ (finRotate 1 : (a : Fin 1) → Fin 1) i = i + 1

Tactic:
@Subsingleton.elim (Fin 1) _ _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin 1
⊢ (finRotate 1 : (a : Fin 1) → Fin 1) i = i + 1

Tactic:
exact @Subsingleton.elim (Fin 1) _ _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n : ℕ
i : Fin (n + 2)
inl :
  (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.last (n + 1)) =
    HAdd.hAdd (α := Fin (n + 2)) (Fin.last (n + 1)) 1
inr : ∀ (h : i < Fin.last (n + 1)), (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1

Tactic:
obtain rfl | h := Fin.eq_or_lt_of_le i.le_last

Premises used: Fin.eq_or_lt_of_le, rfl, Fin.le_last
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n : ℕ
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.last (n + 1)) =
    HAdd.hAdd (α := Fin (n + 2)) (Fin.last (n + 1)) 1

Tactic:
simp [finRotate_last]

Premises used: finRotate_last
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
inr :
  ∀ (val : ℕ) (isLt : val < n + 2) (h : (⟨val, isLt⟩ : Fin (n + 2)) < Fin.last (n + 1)),
    (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) ⟨val, isLt⟩ = (⟨val, isLt⟩ : Fin (n + 2)) + 1
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) i = i + 1

Tactic:
cases i
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n val : ℕ
isLt : val < n + 2
h : (⟨val, isLt⟩ : Fin (n + 2)) < Fin.last (n + 1)
⊢ val < n + 1

Tactic:
simp only [Fin.lt_def, Fin.val_last] at h

Premises used: Fin.lt_def, Fin.val_last
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n_1 n val : ℕ
isLt : val < n + 2
h : val < n + 1
⊢ (finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) ⟨val, isLt⟩ = (⟨val, isLt⟩ : Fin (n + 2)) + 1

Tactic:
simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

Premises used: Fin.add_def, Nat.succ_lt_succ, finRotate_of_lt, Nat.mod_eq_of_lt
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n
⊢ (finRotate n : (a : Fin n) → Fin n) i = i + 1

Tactic:
match n with
  | 0 => exact i.elim0
  | 1 => exact @Subsingleton.elim (Fin 1) _ _ _
  | n + 2 =>
    obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
    · simp [finRotate_last]
    · cases i
      simp only [Fin.lt_def, Fin.val_last] at h
      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i = i + 1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
⊢ Eq (α := Fin n.succ) ((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) 0) 1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
rw : (↑(i + 1) : ℕ) = (↑i : ℕ) + 1
⊢ (↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) = (↑i : ℕ) + 1

Tactic:
rw [finRotate_apply]

Premises used: finRotate_apply
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ (↑i : ℕ) < n

Tactic:
have : (i : ℕ) < n := Fin.val_lt_last h
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : (↑i : ℕ) < n
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1

Tactic:
Fin.val_add_one_of_lt this

Premises used: Fin.val_add_one_of_lt
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
this : (↑i : ℕ) < n
⊢ (↑(i + 1) : ℕ) = (↑i : ℕ) + 1

Tactic:
exact Fin.val_add_one_of_lt this

Premises used: Fin.val_add_one_of_lt
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin n.succ
rw : (↑(i + 1) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
rw₁ rw₂ : (if i = Fin.last n then 0 else (↑i : ℕ) + 1) = if i = Fin.last n then 0 else (↑i : ℕ) + 1
⊢ (↑((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i) : ℕ) = if i = Fin.last n then 0 else (↑i : ℕ) + 1

Tactic:
rw [finRotate_apply, Fin.val_add_one i]

Premises used: Fin.val_add_one, finRotate_apply
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
i : Fin (n + 1)
⊢ i < (finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i ↔ i ≠ Fin.last n

Tactic:
simpa using Fin.lt_last_iff_ne_last

Premises used: Fin.lt_last_iff_ne_last
-- Module: Mathlib.Logic.Equiv.Fin.Rotate
Goal:
n : ℕ
inst : NeZero n
i : Fin n
obtain :
  ∀ (n : ℕ) [inst : NeZero n.succ] (i : Fin n.succ), i < (finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i ↔ i ≠ -1
⊢ i < (finRotate n : (a : Fin n) → Fin n) i ↔ i ≠ -1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl, NeZero.ne