awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n))

Tactic:
⟨fun h => h.symm ▸ monotone_sort f, fun h => unique_monotone h (monotone_sort f)⟩

Premises used: Tuple.unique_monotone, Eq.rec, Iff.intro, Eq.symm, Tuple.monotone_sort
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
rw :
  Eq (α := Fin n → α) (f ∘ (⇑(σ * sort (f ∘ (⇑σ : (a : Fin n) → Fin n))) : (a : Fin n) → Fin n))
    (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))
⊢ Eq (α := Fin n → α)
    (Function.comp (β := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n))
      (⇑(sort (f ∘ (⇑σ : (a : Fin n) → Fin n))) : (a : Fin n) → Fin n))
    (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
rw [Function.comp_assoc, ← Equiv.Perm.coe_mul]

Premises used: Equiv.Perm.coe_mul, Function.comp_assoc
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ Eq (α := Fin n → α) (f ∘ (⇑(σ * sort (f ∘ (⇑σ : (a : Fin n) → Fin n))) : (a : Fin n) → Fin n))
    (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)

Premises used: Tuple.unique_monotone, Function.comp, DFunLike.coe, Tuple.monotone_sort
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ Eq (α := Fin n → α) (f ∘ (⇑(σ * sort (f ∘ (⇑σ : (a : Fin n) → Fin n))) : (a : Fin n) → Fin n))
    (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : Ne (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))
contrapose! :
  ∀ (h : ∀ (i j : Fin n) (_ : i < j), (f ∘ (⇑σ : (a : Fin n) → Fin n)) i ≤ (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
    Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))
⊢ ∃ (i : Fin n) (j : Fin n), i < j ∧ (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i

Tactic:
contrapose! h
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n) (_ : i < j), (f ∘ (⇑σ : (a : Fin n) → Fin n)) i ≤ (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)

Premises used: Iff.mpr, Tuple.comp_sort_eq_comp_iff_monotone, monotone_iff_forall_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n) (_ : i < j), (f ∘ (⇑σ : (a : Fin n) → Fin n)) i ≤ (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ Eq (α := Fin n → α) (f ∘ (⇑σ : (a : Fin n) → Fin n)) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))

Tactic:
exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)

Premises used: Iff.mpr, Tuple.comp_sort_eq_comp_iff_monotone, monotone_iff_forall_lt
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
h : f ≠ f ∘ (⇑(sort f) : (a : Fin n) → Fin n)
⊢ ∃ (i : Fin n) (j : Fin n), i < j ∧ f j < f i

Tactic:
antitone_pair_of_not_sorted' (id h : f ∘ Equiv.refl _ ≠ _)

Premises used: id, Tuple.antitone_pair_of_not_sorted'
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
apply :
  Monotone (α := Fin n) (β := Fin n)
    (Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑σ⁻¹ : (a : Fin n) → Fin n))
apply₁ :
  ∀ (i j : Fin n),
    i < j →
      Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i) : Fin n)
          ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j) : Fin n) →
        LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i : Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j : Fin n)
⊢ sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n) = σ⁻¹

Tactic:
apply (eq_sort_iff.2 ⟨?_ , ?_⟩).symm

Premises used: Iff.mpr, Tuple.eq_sort_iff, And.intro, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
⊢ Monotone (α := Fin n) (β := Fin n)
    (Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑σ⁻¹ : (a : Fin n) → Fin n))

Tactic:
simpa using monotone_id

Premises used: monotone_id
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
i : Fin n
_ :
  ∀ (j : Fin n),
    i < j →
      Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i) : Fin n)
          ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j) : Fin n) →
        LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i : Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j : Fin n)
⊢ ∀ (j : Fin n),
    i < j →
      Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i) : Fin n)
          ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j) : Fin n) →
        LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i : Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j : Fin n)

Tactic:
_
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
i j : Fin n
hij : i < j
h :
  Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i) : Fin n)
    ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j) : Fin n)
⊢ i = j

Tactic:
simpa using h
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
i j : Fin n
hij : i < j
h :
  Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i) : Fin n)
    ((σ : (a : Fin n) → Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j) : Fin n)
⊢ LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) i : Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) j : Fin n)

Tactic:
exact (hij.ne (by simpa using h)).elim

Premises used: False.elim, LT.lt.ne
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
σ : Perm (Fin n)
rw : Eq (α := Perm (Fin n)) (Tuple.sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n)) (Equiv.refl (Fin n)) ↔ σ = 1
rw₁ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ = 1
rw₂ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = 1
rw₃ rw₄ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = Equiv.refl (Fin n)
⊢ Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n) ↔ σ = 1

Tactic:
rw [← Tuple.sort_eq_refl_iff_monotone, Tuple.sort_perm, ← inv_eq_one, one_def]

Premises used: inv_eq_one, Tuple.sort_perm, Equiv.Perm.one_def, Tuple.sort_eq_refl_iff_monotone
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
⊢ take (α := α) m h v i = v (castLE h i)

Tactic:
rfl

Premises used: Fin.take, rfl
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : ∀ (i : Fin 0), take (α := α) 0 ⋯ v i = i.elim0
⊢ take (α := α) 0 ⋯ v = fun (i : Fin 0) ↦ i.elim0

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take (α := α) 0 ⋯ v i = i.elim0

Tactic:
elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take (α := α) 0 ⋯ v i = i.elim0

Tactic:
exact elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
h : ∀ (i : Fin 1), Eq (α := α (castLE ⋯ i)) (take (α := α) 1 ⋯ v i) (v (castLE ⋯ i))
⊢ Eq (α := (i : Fin 1) → α (castLE ⋯ i)) (take (α := α) 1 ⋯ v) fun (i : Fin 1) ↦ v (castLE ⋯ i)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin 1
⊢ Eq (α := α (castLE ⋯ i)) (take (α := α) 1 ⋯ v i) (v (castLE ⋯ i))

Tactic:
simp only [take]

Premises used: Fin.take
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take (α := α) n ⋯ v = init (α := α) v

Tactic:
rfl

Premises used: Fin.init, Fin.take, rfl
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : ∀ (i : Fin n), take (α := α) n ⋯ v i = v i
⊢ take (α := α) n ⋯ v = v

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin n
⊢ take (α := α) n ⋯ v i = v i

Tactic:
simp [take]

Premises used: Fin.take
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m n' : ℕ
h : m ≤ n'
h' : n' ≤ n
v : (i : Fin n) → α i
⊢ take (α := fun (i : Fin n') ↦ α (castLE h' i)) m h (take (α := α) n' h' v) = take (α := α) m ⋯ v

Tactic:
rfl

Premises used: Fin.take, rfl
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
⊢ take (α := fun (i : Fin n) ↦ α i.castSucc) m h (init (α := α) v) = take (α := α) m ⋯ v

Tactic:
rfl

Premises used: Fin.init, Fin.take, rfl
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
h₁ : ∀ (i : Fin (m * n')), take (α := fun (a : Fin (n * n')) ↦ α) (m * n') ⋯ («repeat» n a) i = «repeat» m a i
⊢ take (α := fun (a : Fin (n * n')) ↦ α) (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
i : Fin (m * n')
⊢ take (α := fun (a : Fin (n * n')) ↦ α) (m * n') ⋯ («repeat» n a) i = «repeat» m a i

Tactic:
simp only [take, repeat_apply, modNat, val_castLE]

Premises used: Fin.modNat, Fin.take, Fin.repeat_apply, Fin.val_castLE
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
h₁ :
  ∀ (i : Fin m.succ),
    take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
⊢ take (α := α) m.succ h v = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩)

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h₁ : (↑i : ℕ) = (↑0 : ℕ)
⊢ i = 0

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ (↑i : ℕ) = (↑0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ i = 0

Tactic:
have h' : i = 0 := by ext; simp
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h' : i = 0
h₁ :
  Eq (α := α (castLE h 0)) (take (α := α) (Nat.succ 0) h v 0)
    (snoc (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α (castLE h i)) (take (α := α) 0 ⋯ v) (v ⟨0, h⟩) 0)
⊢ take (α := α) (Nat.succ 0) h v i =
    snoc (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α (castLE h i)) (take (α := α) 0 ⋯ v) (v ⟨0, h⟩) i

Tactic:
subst h'
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
⊢ Eq (α := α (castLE h 0)) (take (α := α) (Nat.succ 0) h v 0)
    (snoc (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α (castLE h i)) (take (α := α) 0 ⋯ v) (v ⟨0, h⟩) 0)

Tactic:
simp [take, snoc, castLE]

Premises used: Fin.castLE, Fin.snoc, Fin.take
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
h_1 :
  ∀ (h : m < n) (i : Fin m.succ),
    take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
h₁ : Eq (α := α (castLE h (last (m + 1)))) (v (castLE h (last (m + 1)))) (v ⟨m + 1, h⟩)
⊢ Eq (α := α (castLE h (last (m + 1)))) (take (α := α) (m + 1).succ h v (last (m + 1)))
    (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) (last (m + 1)))

Tactic:
simp [take, snoc]

Premises used: Fin.snoc, Fin.take
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
h_1 :
  ∀ (h : m < n) (i : Fin m.succ),
    take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ Eq (α := α (castLE h (last (m + 1)))) (v (castLE h (last (m + 1)))) (v ⟨m + 1, h⟩)

Tactic:
congr
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
h_1 :
  ∀ (h : m < n) (i : Fin m.succ),
    take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1)
h_2 :
  Eq (α := α (castLE h i.succ)) (take (α := α) (m + 1).succ h v i.succ)
    (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.succ)
⊢ Eq (α := α (castLE h i.castSucc)) (take (α := α) (m + 1).succ h v i.castSucc)
    (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.castSucc)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
h_1 :
  ∀ (h : m < n) (i : Fin m.succ),
    take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
i : Fin (m + 1).succ
h₁ :
  Eq (α := α (castLE h (last (m + 1)))) (take (α := α) (m + 1).succ h v (last (m + 1)))
    (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) (last (m + 1)))
h₂ :
  ∀ (i : Fin (m + 1)),
    Eq (α := α (castLE h i.succ)) (take (α := α) (m + 1).succ h v i.succ)
        (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.succ) →
      Eq (α := α (castLE h i.castSucc)) (take (α := α) (m + 1).succ h v i.castSucc)
        (snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i.castSucc)
⊢ take (α := α) (m + 1).succ h v i =
    snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i

Tactic:
induction i using reverseInduction with
    | last => simp [take, snoc]; congr
    | cast i _ => simp

Premises used: cast, Fin.snoc, Fin.take, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
i : Fin m.succ
h₁ :
  ∀ (h : 0 < n) (i : Fin (Nat.succ 0)),
    take (α := α) (Nat.succ 0) h v i =
      snoc (α := fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α (castLE h i)) (take (α := α) 0 ⋯ v) (v ⟨0, h⟩) i
h₂ :
  ∀ (m : ℕ),
    (∀ (h : m < n) (i : Fin m.succ),
        take (α := α) m.succ h v i =
          snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i) →
      ∀ (h : m + 1 < n) (i : Fin (m + 1).succ),
        take (α := α) (m + 1).succ h v i =
          snoc (α := fun (i : Fin (m + 1 + 1)) ↦ α (castLE h i)) (take (α := α) (m + 1) ⋯ v) (v ⟨m + 1, h⟩) i
⊢ take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i

Tactic:
induction m with
  | zero =>
    have h' : i = 0 := by ext; simp
    subst h'
    simp [take, snoc, castLE]
  | succ m _ =>
    induction i using reverseInduction with
    | last => simp [take, snoc]; congr
    | cast i _ => simp

Premises used: Fin.succ, Fin.castLE, cast, Fin.snoc, Fin.take, Fin.last
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
h₁ :
  ∀ (j : Fin m),
    take (α := α) m h (update (β := α) v (castLE h i) x) j =
      update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
pos :
  ∀ (h' : j = i),
    take (α := α) m h (update (β := α) v (castLE h i) x) j =
      update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j
neg :
  ∀ (h' : ¬j = i),
    take (α := α) m h (update (β := α) v (castLE h i) x) j =
      update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) j =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j

Tactic:
by_cases h' : j = i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
pos :
  take (α := α) m h (update (β := α) v (castLE h i) x) i =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x i
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) j =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j

Tactic:
rw [h']
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : j = i
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) i =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x i

Tactic:
simp only [take, update_self]

Premises used: Fin.take, Function.update_self
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ castLE h j ≠ castLE h i

Tactic:
simp [h']
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
⊢ castLE h j ≠ castLE h i

Tactic:
have : castLE h j ≠ castLE h i := by simp [h']
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
j : Fin m
h' : ¬j = i
this : castLE h j ≠ castLE h i
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) j =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j

Tactic:
simp only [take, update_of_ne h', update_of_ne this]

Premises used: Fin.take, Function.update_of_ne
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
h₁ : ∀ (j : Fin m), take (α := α) m h (update (β := α) v i x) j = take (α := α) m h v j
⊢ take (α := α) m h (update (β := α) v i x) = take (α := α) m h v

Tactic:
ext j
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
⊢ castLE h j ≠ i

Tactic:
ne_of_val_ne ?_

Premises used: Fin.ne_of_val_ne
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
refine : (↑(castLE h j) : ℕ) ≠ (↑i : ℕ)
⊢ castLE h j ≠ i

Tactic:
refine ne_of_val_ne ?_

Premises used: Fin.ne_of_val_ne
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
simp : (↑j : ℕ) ≠ (↑i : ℕ)
⊢ (↑(castLE h j) : ℕ) ≠ (↑i : ℕ)

Tactic:
simp only [val_castLE]

Premises used: Fin.val_castLE
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
⊢ (↑j : ℕ) ≠ (↑i : ℕ)

Tactic:
Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Premises used: Fin.isLt, Nat.ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
⊢ (↑j : ℕ) ≠ (↑i : ℕ)

Tactic:
exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)

Premises used: Fin.isLt, Nat.ne_of_lt, lt_of_lt_of_le
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
⊢ castLE h j ≠ i

Tactic:
have : castLE h j ≠ i := by
    refine ne_of_val_ne ?_
    simp only [val_castLE]
    exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
j : Fin m
this : castLE h j ≠ i
⊢ take (α := α) m h (update (β := α) v i x) j = take (α := α) m h v j

Tactic:
simp only [take, update_of_ne this]

Premises used: Fin.take, Function.update_of_ne
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
h₁ :
  ∀ (i : Fin m),
    take (α := motive) m ⋯ (fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i) i =
      take (α := fun (i : Fin n) ↦ motive (castAdd n' i)) m h u i
⊢ (take (α := motive) m ⋯ fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i) =
    take (α := fun (i : Fin n) ↦ motive (castAdd n' i)) m h u

Tactic:
ext i
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
⊢ (↑i : ℕ) < n

Tactic:
have : i < n := Nat.lt_of_lt_of_le i.isLt h
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : (↑i : ℕ) < n
h₁ :
  Eq (α := motive (castLE ⋯ i)) (u (castLT (castLE ⋯ i) ⋯) : motive (castAdd n' (castLT (castLE ⋯ i) ⋯)))
    (u (castLE h i))
⊢ take (α := motive) m ⋯ (fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i) i =
    take (α := fun (i : Fin n) ↦ motive (castAdd n' i)) m h u i

Tactic:
simp only [take, addCases, this, val_castLE, ↓reduceDIte]

Premises used: reduceDIte, Fin.take, Fin.val_castLE
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin m
this : (↑i : ℕ) < n
⊢ Eq (α := motive (castLE ⋯ i)) (u (castLT (castLE ⋯ i) ⋯) : motive (castAdd n' (castLT (castLE ⋯ i) ⋯)))
    (u (castLE h i))

Tactic:
congr
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
α : Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → α
v : (i : Fin n') → α
⊢ take (α := fun (a : Fin (n + n')) ↦ α) m ⋯ (append u v) = take (α := fun (i : Fin n) ↦ α) m h u

Tactic:
take_addCases_left m h _ _

Premises used: Fin.take_addCases_left, Fin.append
-- Module: Mathlib.Data.Fin.Tuple.Take
Goal:
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
h₁ :
  ∀ (i : Fin (n + m)),
    take (α := motive) (n + m) ⋯ (fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i)
        i =
      addCases (motive := fun (x : Fin (n + m)) ↦ motive (castLE ⋯ x)) u
        (take (α := fun (i : Fin n') ↦ motive (natAdd n i)) m h v) i
⊢ Eq.{u_2} (α := (i : Fin (n + m)) → motive (castLE ⋯ i))
    (take (α := motive) (n + m) ⋯ fun (i : Fin (n + n')) ↦ addCases (motive := fun (x : Fin (n + n')) ↦ motive x) u v i)
    fun (i : Fin (n + m)) ↦
    addCases (motive := fun (x : Fin (n + m)) ↦ motive (castLE ⋯ x)) u
      (take (α := fun (i : Fin n') ↦ motive (natAdd n i)) m h v) i

Tactic:
ext i