awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
⊢ tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
have pos : ∀ (h : j = i),
  tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
pos :
  ∀ (h : j = i),
    tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
⊢ tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
have neg : ∀ (h : ¬j = i),
  tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (α := α) (update (β := α) q i.succ y) j = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y j
have pos : tail (α := α) (update (β := α) q i.succ y) i = update (β := fun (a : Fin n) ↦ α a.succ) (tail (α := α) q) i y i
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ Eq (α := Fin (n + 1) → β) (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q)
    (cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q))
have h : ∀ (j : Fin (n + 1)),
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have pos : ∀ (h : j = 0), (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
pos :
  ∀ (h : j = 0),
    (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg : ∀ (h : ¬j = 0),
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have pos : comp (α := Fin (n + 1)) g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q) 0 =
  cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (hypothesis)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have this : j'.succ = j
Tactic: have : j'.succ = j := succ_pred j h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
Tactic: rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
neg :
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg₁ : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = (g ∘ q) j'
Tactic: rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
neg :
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
neg₁ : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = (g ∘ q) j'
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg₂ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = (g ∘ q) j'
Tactic: rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
neg :
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
neg₁ : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = (g ∘ q) j'
neg₂ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = (g ∘ q) j'
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg₃ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = g (q j')
Tactic: rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
neg :
  (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j'.succ
neg₁ : (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j'.succ = (g ∘ q) j'
neg₂ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = (g ∘ q) j'
neg₃ : g (cons (α := fun (a : Fin (n + 1)) ↦ α) y q j'.succ) = g (q j')
⊢ (g ∘ cons (α := fun (a : Fin (n + 1)) ↦ α) y q) j = cons (α := fun (i : Fin (n + 1)) ↦ β) (g y) (g ∘ q) j
have neg₄ : g (q j') = g (q j')
Tactic: rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
⊢ g ∘ tail (α := fun (i : Fin (n + 1)) ↦ α) q = tail (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q)
have h : ∀ (j : Fin n), (g ∘ tail (α := fun (i : Fin (n + 1)) ↦ α) q) j = tail (α := fun (a : Fin (n + 1)) ↦ β) (g ∘ q) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ Set.range (ι := Fin (n + 1)) (cons (α := fun (a : Fin n.succ) ↦ α) x b) = insert x (Set.range b)
have rw : insert (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x b 0 : α)
    (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
  insert x (Set.range b)
Tactic: rw [range_fin_succ, cons_zero, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
rw :
  insert (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x b 0 : α)
      (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
    insert x (Set.range b)
⊢ Set.range (ι := Fin (n + 1)) (cons (α := fun (a : Fin n.succ) ↦ α) x b) = insert x (Set.range b)
have rw₁ : insert x (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
  insert x (Set.range b)
Tactic: rw [range_fin_succ, cons_zero, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
rw :
  insert (α := α) (cons (α := fun (a : Fin n.succ) ↦ α) x b 0 : α)
      (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
    insert x (Set.range b)
rw₁ :
  insert x (Set.range (ι := Fin n) (tail (α := fun (i : Fin (n + 1)) ↦ α) (cons (α := fun (a : Fin n.succ) ↦ α) x b))) =
    insert x (Set.range b)
⊢ Set.range (ι := Fin (n + 1)) (cons (α := fun (a : Fin n.succ) ↦ α) x b) = insert x (Set.range b)
have rw₂ : insert x (Set.range b) = insert x (Set.range b)
Tactic: rw [range_fin_succ, cons_zero, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m
have rw : m + 0 = m
Tactic: rw [hv, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
rw : m + 0 = m
⊢ m + n = m
have rw₁ : m = m
Tactic: rw [hv, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯
have refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (u ∘ Fin.cast sorry) (castAdd n l)
Tactic: refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)
⊢ append u v = u ∘ Fin.cast ⋯
have refine_2 : ∀ (r : Fin n), append u v (natAdd m r) = (u ∘ Fin.cast sorry) (natAdd m r)
Tactic: refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)
have refine_1 : u l = u (Fin.cast sorry (castAdd n l))
Tactic: rw [append_left, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))
have refine_1 : (↑l : ℕ) = (↑(Fin.cast sorry (castAdd n l)) : ℕ)
Tactic: refine congr_arg u (Fin.ext ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ m + n = n
have rw : 0 + n = n
Tactic: rw [hu, Nat.zero_add]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α_1 : Fin (n + 1) → Sort u
x : α_1 0
q : (i : Fin (n + 1)) → α_1 i
p : (i : Fin n) → α_1 i.succ
i : Fin n
y : α_1 i.succ
z : α_1 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
rw : 0 + n = n
⊢ m + n = n
have rw₁ : n = n
Tactic: rw [hu, Nat.zero_add]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯
have refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (v ∘ Fin.cast sorry) (castAdd n l)
Tactic: refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
refine_1 : ∀ (l : Fin m), append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)
⊢ append u v = v ∘ Fin.cast ⋯
have refine_2 : ∀ (r : Fin n), append u v (natAdd m r) = (v ∘ Fin.cast sorry) (natAdd m r)
Tactic: refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)
have refine_2 : v r = v (Fin.cast sorry (natAdd m r))
Tactic: rw [append_right, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))
have refine_2 : (↑r : ℕ) = (↑(Fin.cast sorry (natAdd m r)) : ℕ)
Tactic: refine congr_arg v (Fin.ext ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯
have h : ∀ (i : Fin (m + n + p)), append (append a b) c i = (append a (append b c) ∘ Fin.cast sorry) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = (append a (append b c) ∘ Fin.cast ⋯) i
have h : append (append a b) c i = append a (append b c) (Fin.cast sorry i)
Tactic: rw [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)
have h : ∀ (l : Fin (m + n)), append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast sorry (castAdd p l))
Tactic: refine Fin.addCases (fun l => ?_) (fun r => ?_) i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
h : ∀ (l : Fin (m + n)), append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)
have h₁ : ∀ (r : Fin p), append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast sorry (natAdd (m + n) r))
Tactic: refine Fin.addCases (fun l => ?_) (fun r => ?_) i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))
have h : append a b l = append a (append b c) (Fin.cast sorry (castAdd p l))
Tactic: rw [append_left]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))
have h : ∀ (ll : Fin m), append a b (castAdd n ll) = append a (append b c) (Fin.cast sorry (castAdd p (castAdd n ll)))
Tactic: refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
h : ∀ (ll : Fin m), append a b (castAdd n ll) = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))
have h₁ : ∀ (lr : Fin n), append a b (natAdd m lr) = append a (append b c) (Fin.cast sorry (castAdd p (natAdd m lr)))
Tactic: refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ append a b (castAdd n ll) = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
have h : a ll = append a (append b c) (Fin.cast sorry (castAdd p (castAdd n ll)))
Tactic: rw [append_left]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))
have h : b lr = append a (append b c) (Fin.cast sorry (castAdd p (natAdd m lr)))
Tactic: rw [append_right]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
have h : c r = append a (append b c) (Fin.cast sorry (natAdd (m + n) r))
Tactic: rw [append_right]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ append x₀ x = cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯
have h : ∀ (i : Fin (1 + n)), append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast sorry) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
⊢ append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) i
have h : ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast sorry) (castAdd n i)
Tactic: refine Fin.addCases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin (1 + n)
h :
  ∀ (i : Fin 1), append x₀ x (castAdd n i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)
⊢ append x₀ x i = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) i
have h₁ : ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast sorry) (natAdd 1 i)
Tactic: refine Fin.addCases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)
have h : cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x (Fin.cast sorry (castAdd n 0)) = x₀ 0
Tactic: rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ append x₀ x (natAdd 1 i) = (cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)
have h : cons (α := fun (a : Fin (n + 1)) ↦ α) (x₀ 0) x i.succ = x i
Tactic: rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
⊢ cons (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x xs =
    append (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0) xs ∘ Fin.cast ⋯
have h : ∀ (i : Fin (n + 1)),
  cons (α := fun (a : Fin (n + HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x xs i =
    (append (cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ α) x elim0) xs ∘ Fin.cast sorry) i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m_1 n_1 : ℕ
α_1 : Fin (n_1 + 1) → Sort u
x : α_1 0
q : (i : Fin (n_1 + 1)) → α_1 i
p : (i : Fin n_1) → α_1 i.succ
i : Fin n_1
y : α_1 i.succ
z : α_1 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m
have rw : n + m = n + m
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯
have subst : ∀ (xs : Fin n' → α), append (xs ∘ Fin.cast sorry) ys = append xs ys ∘ Fin.cast sorry
Tactic: subst h
Cleared hypotheses: n, xs, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m_1 n_1 : ℕ
α_1 : Fin (n_1 + 1) → Sort u
x : α_1 0
q : (i : Fin (n_1 + 1)) → α_1 i
p : (i : Fin n_1) → α_1 i.succ
i : Fin n_1
y : α_1 i.succ
z : α_1 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m' = n + m
have rw : n + m = n + m
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ append xs (ys ∘ Fin.cast h) = append xs ys ∘ Fin.cast ⋯
have subst : ∀ (ys : Fin m' → α), append xs (ys ∘ Fin.cast sorry) = append xs ys ∘ Fin.cast sorry
Tactic: subst h
Cleared hypotheses: m, ys, h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i)
have rcases : ∀ (i : Fin (m + n)), append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast sorry i.rev)
Tactic: rcases rev_surjective i with ⟨i, rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
have rw : append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast sorry i.rev)
Tactic: rw [rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
have left : ∀ (i : Fin m), append xs ys (castAdd n i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast sorry (castAdd n i).rev)
Tactic: induction i using Fin.addCases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
left : ∀ (i : Fin m), append xs ys (castAdd n i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i).rev)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
have right : ∀ (i : Fin n), append xs ys (natAdd m i) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast sorry (natAdd m i).rev)
Tactic: induction i using Fin.addCases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (append (fun (i : Fin m) ↦ f (castAdd n i)) fun (i : Fin n) ↦ f (natAdd m i)) = f
have unfold : (fun (i : Fin (m + n)) ↦
    if hi : (↑i : ℕ) < m then
      Eq.rec (motive := fun (x : Fin (m + n)) (h : castAdd n (i.castLT hi) = x) ↦ (fun (x : Fin (m + n)) ↦ α) x)
        ((fun (i : Fin m) ↦ f (castAdd n i)) (i.castLT hi)) sorry
    else
      Eq.rec (motive := fun (x : Fin (m + n)) (h : natAdd m (subNat m (Fin.cast sorry i) sorry) = x) ↦
        (fun (x : Fin (m + n)) ↦ α) x) ((fun (i : Fin n) ↦ f (natAdd m i)) (subNat m (Fin.cast sorry i) sorry)) sorry) =
  f
Tactic: unfold append addCases
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
⊢ (fun (i : Fin (m + n)) ↦
      addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
        (fun (j : Fin n) ↦ v (natAdd m j)) i) =
    v
have h : ∀ (i : Fin (m + n)),
  addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) i =
    v i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Basic (goal)
Goal:
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i : Fin (m + n)
⊢ addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) i =
    v i
have h : ∀ (i : Fin m),
  addCases (motive := fun (x : Fin (m + n)) ↦ γ x) (fun (i : Fin m) ↦ v (castAdd n i))
      (fun (j : Fin n) ↦ v (natAdd m j)) (castAdd n i) =
    v (castAdd n i)
Tactic: cases i using addCases
Cleared hypotheses: i