awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
refine_1 :
  ∀ (h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)))
    (i j : Fin n) (hij : i < j) (hfij : f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j)),
    LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
have refine_2 : ∀
  (h :
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n))
  (i j : Fin n) (hij : i < j),
  LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
Tactic: refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
have refine_2 : ∀ (he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
  LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
Tactic: obtain he | hl := (h.1 hij.le).eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
refine_2 :
  ∀ (he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
    LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
      ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
have refine_2₁ : ∀ (hl : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i < (f ∘ (⇑σ : (a : Fin n) → Fin n)) j),
  LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
Tactic: obtain he | hl := (h.1 hij.le).eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
he : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i = (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
have refine_2 : ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
    ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
  ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
    LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)
Tactic: apply Prod.Lex.toLex_lt_toLex.2
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h :
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
i j : Fin n
hij : i < j
hl : (f ∘ (⇑σ : (a : Fin n) → Fin n)) i < (f ∘ (⇑σ : (a : Fin n) → Fin n)) j
⊢ LT.lt (α := ↥(graph f)) ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) i : ↥(graph f))
    ((Equiv.trans σ (graphEquiv₁ f) : (a : Fin n) → ↥(graph f)) j : ↥(graph f))
have refine_2 : ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 <
    ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∨
  ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i) : α × Fin n).1 =
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j) : α × Fin n).1 ∧
    LT.lt (α := Fin n) ((f ((σ : (a : Fin n) → Fin n) i), (σ : (a : Fin n) → Fin n) i).2 : Fin n)
      ((f ((σ : (a : Fin n) → Fin n) j), (σ : (a : Fin n) → Fin n) j).2 : Fin n)
Tactic: apply Prod.Lex.toLex_lt_toLex.2
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ sort f = Equiv.refl (Fin n) ↔ Monotone f
have rw : (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
Tactic: rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp_id]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f
have simp : Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j
Tactic: simp only [id, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (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))
have 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))
Tactic: rw [Function.comp_assoc, ← Equiv.Perm.coe_mul]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
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))
⊢ ∃ (i : Fin n) (j : Fin n), i < j ∧ (f ∘ (⇑σ : (a : Fin n) → Fin n)) j < (f ∘ (⇑σ : (a : Fin n) → Fin n)) i
have 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))
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
σ : Equiv.Perm (Fin n)
⊢ sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n) = σ⁻¹
have apply : Monotone (α := Fin n) (β := Fin n) (Function.comp (β := Fin n) (⇑σ : (a : Fin n) → Fin n) (⇑σ⁻¹ : (a : Fin n) → Fin n))
Tactic: apply (eq_sort_iff.2 ⟨?_ , ?_⟩).symm
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
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))
⊢ sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n) = σ⁻¹
have 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)
Tactic: apply (eq_sort_iff.2 ⟨?_ , ?_⟩).symm
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n) ↔ σ = 1
have rw : Eq (α := Perm (Fin n)) (Tuple.sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n)) (Equiv.refl (Fin n)) ↔ σ = 1
Tactic: rw [← Tuple.sort_eq_refl_iff_monotone, Tuple.sort_perm, ← inv_eq_one, one_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
rw : Eq (α := Perm (Fin n)) (Tuple.sort (α := Fin n) (⇑σ : (a : Fin n) → Fin n)) (Equiv.refl (Fin n)) ↔ σ = 1
⊢ Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n) ↔ σ = 1
have rw₁ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ = 1
Tactic: rw [← Tuple.sort_eq_refl_iff_monotone, Tuple.sort_perm, ← inv_eq_one, one_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
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
⊢ Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n) ↔ σ = 1
have rw₂ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = 1
Tactic: rw [← Tuple.sort_eq_refl_iff_monotone, Tuple.sort_perm, ← inv_eq_one, one_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
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
⊢ Monotone (α := Fin n) (β := Fin n) (⇑σ : (a : Fin n) → Fin n) ↔ σ = 1
have rw₃ : σ⁻¹ = Equiv.refl (Fin n) ↔ σ⁻¹ = Equiv.refl (Fin n)
Tactic: rw [← Tuple.sort_eq_refl_iff_monotone, Tuple.sort_perm, ← inv_eq_one, one_def]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take (α := α) 0 ⋯ v = fun (i : Fin 0) ↦ i.elim0
have h : ∀ (i : Fin 0), take (α := α) 0 sorry v i = i.elim0
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ Eq (α := (i : Fin 1) → α (castLE ⋯ i)) (take (α := α) 1 ⋯ v) fun (i : Fin 1) ↦ v (castLE ⋯ i)
have h : ∀ (i : Fin 1), Eq (α := α (castLE sorry i)) (take (α := α) 1 sorry v i) (v (castLE sorry i))
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take (α := α) n ⋯ v = v
have h : ∀ (i : Fin n), take (α := α) n sorry v i = v i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (α := fun (a : Fin (n * n')) ↦ α) (m * n') ⋯ («repeat» n a) = «repeat» m a
have h₁ : ∀ (i : Fin (m * n')), take (α := fun (a : Fin (n * n')) ↦ α) (m * n') sorry («repeat» n a) i = «repeat» m a i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
⊢ take (α := α) m.succ h v = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩)
have h₁ : ∀ (i : Fin m.succ),
  take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m sorry v) (v ⟨m, h⟩) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ i = 0
have h₁ : (↑i : ℕ) = (↑0 : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (hypothesis)
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
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
have h' : i = 0
Tactic: have h' : i = 0 := by ext; simp
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
h' : i = 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
have 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 sorry v) (v ⟨0, h⟩) 0)
Tactic: subst h'
Cleared hypotheses: i, h'
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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)))) (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)))
have h₁ : Eq (α := α (castLE h (last (m + 1)))) (v (castLE h (last (m + 1)))) (v ⟨m + 1, h⟩)
Tactic: simp [take, snoc]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
⊢ 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
have 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) sorry v) (v ⟨m + 1, h⟩) (last (m + 1)))
Tactic: induction i using reverseInduction with
    | last => simp [take, snoc]; congr
    | cast i _ => simp
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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)))
⊢ 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
have 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) sorry 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) sorry v) (v ⟨m + 1, h⟩) i.castSucc)
Tactic: induction i using reverseInduction with
    | last => simp [take, snoc]; congr
    | cast i _ => simp
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m < n
v : (i : Fin n) → α i
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
have 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 sorry v) (v ⟨0, 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
Cleared hypotheses: m, h, i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
⊢ take (α := α) m.succ h v i = snoc (α := fun (i : Fin (m + 1)) ↦ α (castLE h i)) (take (α := α) m ⋯ v) (v ⟨m, h⟩) i
have 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 sorry 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) sorry v) (v ⟨m + 1, 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
Cleared hypotheses: m, h, i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin m
x : α (castLE h i)
⊢ take (α := α) m h (update (β := α) v (castLE h i) x) =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x
have 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
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
⊢ 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
have 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
Tactic: by_cases h' : j = i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
⊢ 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
have 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
Tactic: by_cases h' : j = i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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) j =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j
have 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
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (hypothesis)
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) j =
    update (β := fun (a : Fin m) ↦ α (castLE h a)) (take (α := α) m h v) i x j
have this : castLE h j ≠ castLE h i
Tactic: have : castLE h j ≠ castLE h i := by simp [h']
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
Goal:
n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : (↑i : ℕ) ≥ m
x : α i
⊢ take (α := α) m h (update (β := α) v i x) = take (α := α) m h v
have h₁ : ∀ (j : Fin m), take (α := α) m h (update (β := α) v i x) j = take (α := α) m h v j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
have refine : (↑(castLE h j) : ℕ) ≠ (↑i : ℕ)
Tactic: refine ne_of_val_ne ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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 : ℕ)
have simp : (↑j : ℕ) ≠ (↑i : ℕ)
Tactic: simp only [val_castLE]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (hypothesis)
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
⊢ take (α := α) m h (update (β := α) v i x) j = take (α := α) m h v j
have this : 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)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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)
⊢ (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
have h₁ : ∀ (i : Fin m),
  take (α := motive) m sorry (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: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (hypothesis)
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
⊢ 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
have this : (↑i : ℕ) < n
Tactic: have : i < n := Nat.lt_of_lt_of_le i.isLt h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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
⊢ 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
have h₁ : Eq (α := motive (castLE sorry i)) (u (castLT (castLE sorry i) sorry) : motive (castAdd n' (castLT (castLE sorry i) sorry))) (u (castLE h i))
Tactic: simp only [take, addCases, this, val_castLE, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Take (goal)
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)
⊢ 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
have h₁ : ∀ (i : Fin (n + m)),
  take (α := motive) (n + m) sorry (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 sorry x)) u
      (take (α := fun (i : Fin n') ↦ motive (natAdd n i)) m h v) i
Tactic: ext i