[GOAL]
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
α : TypeVec n
β : TypeVec n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i
[PROOFSTEP]
apply h
[GOAL]
n : ℕ
α : TypeVec (n + 1)
i : Fin2 (n + 1)
⊢ (drop α ::: last α) i = α i
[PROOFSTEP]
cases i
[GOAL]
case fz
n : ℕ
α : TypeVec (n + 1)
⊢ (drop α ::: last α) Fin2.fz = α Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case fs
n : ℕ
α : TypeVec (n + 1)
a✝ : Fin2 (Nat.add n 0)
⊢ (drop α ::: last α) (Fin2.fs a✝) = α (Fin2.fs a✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
C : TypeVec (n + 1) → Sort u
H : (α : TypeVec n) → (β : Type ?u.25747) → C (α ::: β)
γ : TypeVec (n + 1)
⊢ C γ
[PROOFSTEP]
rw [← @append1_drop_last _ γ]
[GOAL]
n : ℕ
C : TypeVec (n + 1) → Sort u
H : (α : TypeVec n) → (β : Type ?u.25747) → C (α ::: β)
γ : TypeVec (n + 1)
⊢ C (drop γ ::: last γ)
[PROOFSTEP]
apply H
[GOAL]
n : ℕ
α : TypeVec 0
β : TypeVec 0
i : Fin2 0
⊢ α i → β i
[PROOFSTEP]
apply Fin2.elim0 i
[GOAL]
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x
[PROOFSTEP]
cases x
[GOAL]
case fz
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz
[PROOFSTEP]
apply h₁
[GOAL]
case fs
n : ℕ
α : TypeVec (n + 1)
β : TypeVec (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 (Nat.add n 0)
⊢ f (Fin2.fs a✝) = g (Fin2.fs a✝)
[PROOFSTEP]
apply congr_fun h₀
[GOAL]
n : ℕ
α : TypeVec (n + 1)
α' : TypeVec (n + 1)
f f' : drop α ⟹ drop α'
g g' : last α → last α'
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'
[PROOFSTEP]
rw [← dropFun_splitFun f g, H, ← lastFun_splitFun f g, H]
[GOAL]
n : ℕ
α : TypeVec (n + 1)
α' : TypeVec (n + 1)
f f' : drop α ⟹ drop α'
g g' : last α → last α'
H : splitFun f g = splitFun f' g'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α₀ : TypeVec 0
f₀ : α₀ ⟹ Fin2.elim0
x : Fin2 0
⊢ (nilFun ⊚ f₀) x = f₀ x
[PROOFSTEP]
apply Fin2.elim0 x
[GOAL]
n : ℕ
a✝ b : TypeVec 0
a : Fin2 0
⊢ a✝ a = b a
[PROOFSTEP]
apply Fin2.elim0 a
[GOAL]
n : ℕ
β : TypeVec 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec 0
⊢ β Fin2.elim0 = β v
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
β : TypeVec 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec 0
⊢ Fin2.elim0 = v
[PROOFSTEP]
funext i
[GOAL]
case e_a.h
n : ℕ
β : TypeVec 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec 0
i : Fin2 0
⊢ Fin2.elim0 i = v i
[PROOFSTEP]
cases i
[GOAL]
n✝ n : ℕ
β : TypeVec (n + 1) → Sort u_1
f : (t : Type ?u.47809) → (v : TypeVec n) → β (v ::: t)
v : TypeVec (n + 1)
⊢ β (drop v ::: last v) = β v
[PROOFSTEP]
simp
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
⊢ β v v' fs
[PROOFSTEP]
refine' cast _ f
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
[PROOFSTEP]
have eq₁ : v = Fin2.elim0 := by funext i; contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
⊢ v = Fin2.elim0
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
i : Fin2 0
⊢ v i = Fin2.elim0 i
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
[PROOFSTEP]
have eq₂ : v' = Fin2.elim0 := by funext i; contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
⊢ v' = Fin2.elim0
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
i : Fin2 0
⊢ v' i = Fin2.elim0 i
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
[PROOFSTEP]
have eq₃ : fs = nilFun := by funext i; contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
⊢ fs = nilFun
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
i : Fin2 0
⊢ fs i = nilFun i
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec 0
v' : TypeVec 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β v v' fs
[PROOFSTEP]
cases eq₁
[GOAL]
case refl
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v' : TypeVec 0
eq₂ : v' = Fin2.elim0
fs : Fin2.elim0 ⟹ v'
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 v' fs
[PROOFSTEP]
cases eq₂
[GOAL]
case refl.refl
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
fs : Fin2.elim0 ⟹ Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 fs
[PROOFSTEP]
cases eq₃
[GOAL]
case refl.refl.refl
n : ℕ
β : (v : TypeVec 0) → (v' : TypeVec 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 nilFun
[PROOFSTEP]
rfl
[GOAL]
n✝ n : ℕ
β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.50165) →
    (t' : Type ?u.50168) →
      (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
⊢ (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → (fs : v ⟹ v') → β v v' fs
[PROOFSTEP]
intro v v'
[GOAL]
n✝ n : ℕ
β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.50165) →
    (t' : Type ?u.50168) →
      (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec (n + 1)
v' : TypeVec (n + 1)
⊢ (fs : v ⟹ v') → β v v' fs
[PROOFSTEP]
rw [← append1_drop_last v, ← append1_drop_last v']
[GOAL]
n✝ n : ℕ
β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.50165) →
    (t' : Type ?u.50168) →
      (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec (n + 1)
v' : TypeVec (n + 1)
⊢ (fs : drop v ::: last v ⟹ drop v' ::: last v') → β (drop v ::: last v) (drop v' ::: last v') fs
[PROOFSTEP]
intro fs
[GOAL]
n✝ n : ℕ
β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.50165) →
    (t' : Type ?u.50168) →
      (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec (n + 1)
v' : TypeVec (n + 1)
fs : drop v ::: last v ⟹ drop v' ::: last v'
⊢ β (drop v ::: last v) (drop v' ::: last v') fs
[PROOFSTEP]
rw [← split_dropFun_lastFun fs]
[GOAL]
n✝ n : ℕ
β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.50165) →
    (t' : Type ?u.50168) →
      (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
v : TypeVec (n + 1)
v' : TypeVec (n + 1)
fs : drop v ::: last v ⟹ drop v' ::: last v'
⊢ β (drop v ::: last v) (drop v' ::: last v') (splitFun (dropFun fs) (lastFun fs))
[PROOFSTEP]
apply F
[GOAL]
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
⊢ (f : Fin2.elim0 ⟹ Fin2.elim0) → β f
[PROOFSTEP]
intro g
[GOAL]
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
⊢ β g
[PROOFSTEP]
have : g = nilFun
[GOAL]
case this
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
⊢ g = nilFun
n : ℕ β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1 f : β nilFun g : Fin2.elim0 ⟹ Fin2.elim0 this : g = nilFun ⊢ β g
[PROOFSTEP]
ext ⟨⟩
[GOAL]
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β g
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β nilFun
[PROOFSTEP]
exact f
[GOAL]
n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec n
v' : TypeVec n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
⊢ (fs : v ::: t ⟹ v' ::: t') → β fs
[PROOFSTEP]
intro fs
[GOAL]
n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec n
v' : TypeVec n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β fs
[PROOFSTEP]
rw [← split_dropFun_lastFun fs]
[GOAL]
n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec n
v' : TypeVec n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
fs : v ::: t ⟹ v' ::: t'
⊢ β (splitFun (dropFun fs) (lastFun fs))
[PROOFSTEP]
apply F
[GOAL]
n✝ : ℕ
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 => x)
[PROOFSTEP]
ext i : 1
[GOAL]
case a
n✝ : ℕ
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 => x) i
[PROOFSTEP]
cases i
[GOAL]
case a.fz
n✝ : ℕ
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec n
⊢ TypeVec.const x (α ::: β) Fin2.fz = (TypeVec.const x α ::: fun x_1 => x) Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case a.fs
n✝ : ℕ
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec n
a✝ : Fin2 (Nat.add n 0)
⊢ TypeVec.const x (α ::: β) (Fin2.fs a✝) = (TypeVec.const x α ::: fun x_1 => x) (Fin2.fs a✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec 0
β : TypeVec 0
f : α ⟹ β
⊢ f = nilFun
[PROOFSTEP]
ext x
[GOAL]
case a.h
n : ℕ
α : TypeVec 0
β : TypeVec 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝
[PROOFSTEP]
cases x
[GOAL]
n : ℕ
α : TypeVec 0
⊢ id = nilFun
[PROOFSTEP]
ext x
[GOAL]
case a.h
n : ℕ
α : TypeVec 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x x✝
[PROOFSTEP]
cases x
[GOAL]
n : ℕ
β : Type u_1
x : β
α : TypeVec 0
⊢ TypeVec.const x α = nilFun
[PROOFSTEP]
ext i : 1
[GOAL]
case a
n : ℕ
β : Type u_1
x : β
α : TypeVec 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i
[PROOFSTEP]
cases i
[GOAL]
n✝ : ℕ
β : Type u_1
n : ℕ
α : TypeVec n
⊢ repeatEq (α ::: β) = splitFun (repeatEq α) (uncurry Eq)
[PROOFSTEP]
induction n
[GOAL]
case zero
n : ℕ
β : Type u_1
α : TypeVec zero
⊢ repeatEq (α ::: β) = splitFun (repeatEq α) (uncurry Eq)
[PROOFSTEP]
rfl
[GOAL]
case succ
n : ℕ
β : Type u_1
n✝ : ℕ
n_ih✝ : ∀ (α : TypeVec n✝), repeatEq (α ::: β) = splitFun (repeatEq α) (uncurry Eq)
α : TypeVec (succ n✝)
⊢ repeatEq (α ::: β) = splitFun (repeatEq α) (uncurry Eq)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec 0
⊢ repeatEq α = nilFun
[PROOFSTEP]
ext i
[GOAL]
case a.h
n : ℕ
α : TypeVec 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ repeatEq α i x✝ = nilFun i x✝
[PROOFSTEP]
cases i
[GOAL]
n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p
[PROOFSTEP]
induction i
[GOAL]
case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
[PROOFSTEP]
case fz => rfl
[GOAL]
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
[PROOFSTEP]
case fz => rfl
[GOAL]
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
[PROOFSTEP]
rfl
[GOAL]
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
[PROOFSTEP]
case fs _ ih => erw [TypeVec.const, @ih (drop α) x]
[GOAL]
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
[PROOFSTEP]
case fs _ ih => erw [TypeVec.const, @ih (drop α) x]
[GOAL]
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
[PROOFSTEP]
erw [TypeVec.const, @ih (drop α) x]
[GOAL]
n : ℕ
α β : TypeVec n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case fz
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝ : α✝ i
b✝ : β✝ i
n✝ : ℕ
α β : TypeVec (succ n✝)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
[PROOFSTEP]
simp_all only [prod.fst, prod.mk]
[GOAL]
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α β : TypeVec n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd i (prod.mk i a b) = b
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case fz
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝ : α✝ i
b✝ : β✝ i
n✝ : ℕ
α β : TypeVec (succ n✝)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.snd Fin2.fz (prod.mk Fin2.fz a b) = b
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.snd a✝ (prod.mk a✝ a b) = b
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.snd (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = b
[PROOFSTEP]
simp_all [prod.snd, prod.mk]
[GOAL]
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.snd a✝ (prod.mk a✝ a b) = b
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.snd (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = b
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.fst ⊚ (f ⊗' g) = f ⊚ prod.fst
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i
[PROOFSTEP]
induction i
[GOAL]
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) (Fin2.fs a✝) = (f ⊚ prod.fst) (Fin2.fs a✝)
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) Fin2.fz = (f ⊚ prod.fst) Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) (Fin2.fs a✝) = (f ⊚ prod.fst) (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) (Fin2.fs a✝) = (f ⊚ prod.fst) (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.fst ⊚ (f ⊗' g)) a✝ = (f ⊚ prod.fst) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.fst ⊚ (f ⊗' g)) (Fin2.fs a✝) = (f ⊚ prod.fst) (Fin2.fs a✝)
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.snd ⊚ (f ⊗' g) = g ⊚ prod.snd
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
α α' β β' : TypeVec n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
[PROOFSTEP]
induction i
[GOAL]
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec (succ n✝)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) (Fin2.fs a✝) = (g ⊚ prod.snd) (Fin2.fs a✝)
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α : TypeVec n
⊢ prod.fst ⊚ prod.diag = id
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
α : TypeVec n
i : Fin2 n
⊢ (prod.fst ⊚ prod.diag) i = id i
[PROOFSTEP]
induction i
[GOAL]
case h.fz
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.fst ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α : TypeVec n
⊢ prod.snd ⊚ prod.diag = id
[PROOFSTEP]
funext i
[GOAL]
case h
n : ℕ
α : TypeVec n
i : Fin2 n
⊢ (prod.snd ⊚ prod.diag) i = id i
[PROOFSTEP]
induction i
[GOAL]
case h.fz
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz
[PROOFSTEP]
case fz => rfl
[GOAL]
n n✝ : ℕ
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) Fin2.fz = id Fin2.fz
[PROOFSTEP]
rfl
[GOAL]
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
case fs _ _ i_ih => apply i_ih
[GOAL]
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝}, (prod.snd ⊚ prod.diag) a✝ = id a✝
α : TypeVec (succ n✝)
⊢ (prod.snd ⊚ prod.diag) (Fin2.fs a✝) = id (Fin2.fs a✝)
[PROOFSTEP]
apply i_ih
[GOAL]
n : ℕ
α : TypeVec n
i : Fin2 n
x y : α i
⊢ ofRepeat (repeatEq α i (prod.mk i x y)) ↔ x = y
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case fz
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x y : α Fin2.fz
⊢ ofRepeat (repeatEq α Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y
case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
[PROOFSTEP]
rfl
[GOAL]
case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
[PROOFSTEP]
erw [repeatEq, i_ih]
[GOAL]
n✝¹ n : ℕ
α✝ : TypeVec n
p✝ : α✝ ⊗ α✝ ⟹ repeat n Prop
n✝ : ℕ
α : TypeVec (succ n✝)
p : α ⊗ α ⟹ repeat (succ n✝) Prop
x : (fun i => { x // ofRepeat (p i (prod.mk i x.fst x.snd)) }) Fin2.fz
⊢ ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).fst (↑x).snd)) = p Fin2.fz ↑x
[PROOFSTEP]
congr
[GOAL]
n✝¹ n : ℕ
α✝ : TypeVec n
p✝ : α✝ ⊗ α✝ ⟹ repeat n Prop
n✝ : ℕ
α : TypeVec (succ n✝)
p : α ⊗ α ⟹ repeat (succ n✝) Prop
x : Subtype_ p Fin2.fz
⊢ p Fin2.fz ↑x = ofRepeat (p Fin2.fz (prod.mk Fin2.fz (↑x).fst (↑x).snd))
[PROOFSTEP]
congr
[GOAL]
n : ℕ
α : TypeVec 0
ps : α ⟹ repeat 0 Prop
⊢ ∀ (x : Fin2 0), subtypeVal ps x = nilFun x
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n✝ n : ℕ
α : TypeVec n
⊢ subtypeVal (repeatEq α) ⊚ diagSub = prod.diag
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n✝ n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) i x = prod.diag i x
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case a.h.fz
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x
case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
[PROOFSTEP]
simp [prod.diag, diagSub, repeatEq, subtypeVal, comp]
[GOAL]
case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
[PROOFSTEP]
apply @i_ih (drop α)
[GOAL]
n : ℕ
⊢ ∀ {n : ℕ} {α β : TypeVec n}, (id ⊗' id) = id
[PROOFSTEP]
intros
[GOAL]
n n✝ : ℕ
α✝ β✝ : TypeVec n✝
⊢ (id ⊗' id) = id
[PROOFSTEP]
ext i a
[GOAL]
case a.h
n n✝ : ℕ
α✝ β✝ : TypeVec n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case a.h.fz
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a
[PROOFSTEP]
cases a
[GOAL]
case a.h.fz.mk
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
fst✝ : last α✝
snd✝ : last β✝
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝¹ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) (Fin2.fs a✝)
⊢ (id ⊗' id) (Fin2.fs a✝) a = id (Fin2.fs a✝) a
[PROOFSTEP]
apply i_ih
[GOAL]
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))
[PROOFSTEP]
ext i a
[GOAL]
case a.h
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a
[PROOFSTEP]
cases i
[GOAL]
case a.h.fz
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a
[PROOFSTEP]
cases a
[GOAL]
case a.h.fz.mk
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n✝ n : ℕ
α α' β β' : TypeVec n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 (Nat.add n 0)
a : ((α ⊗ β) ::: (φ × ψ)) (Fin2.fs a✝)
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) (Fin2.fs a✝) a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) (Fin2.fs a✝) a
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec (n + 1)
⊢ dropFun prod.diag = prod.diag
[PROOFSTEP]
ext i : 2
[GOAL]
case a.h
n : ℕ
α : TypeVec (n + 1)
i : Fin2 n
x✝ : drop α i
⊢ dropFun prod.diag i x✝ = prod.diag i x✝
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
x✝ : drop α Fin2.fz
⊢ dropFun prod.diag Fin2.fz x✝ = prod.diag Fin2.fz x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec (n✝ + 1)} (x : drop α a✝), dropFun prod.diag a✝ x = prod.diag a✝ x
α : TypeVec (Nat.succ n✝ + 1)
x✝ : drop α (Fin2.fs a✝)
⊢ dropFun prod.diag (Fin2.fs a✝) x✝ = prod.diag (Fin2.fs a✝) x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
x✝ : drop α Fin2.fz
⊢ prod.diag (Fin2.fs Fin2.fz) x✝ = prod.diag Fin2.fz x✝
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec (n✝ + 1)} (x : drop α a✝), dropFun prod.diag a✝ x = prod.diag a✝ x
α : TypeVec (Nat.succ n✝ + 1)
x✝ : drop α (Fin2.fs a✝)
⊢ prod.diag (Fin2.fs (Fin2.fs a✝)) x✝ = prod.diag (Fin2.fs a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ dropFun (toSubtype p) = toSubtype fun i x => p (Fin2.fs i) x
[PROOFSTEP]
ext i
[GOAL]
case a.h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : Fin2 n
x✝ : drop (fun i => { x // ofRepeat (p i x) }) i
⊢ dropFun (toSubtype p) i x✝ = toSubtype (fun i x => p (Fin2.fs i) x) i x✝
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (fun i => { x // ofRepeat (p i x) }) Fin2.fz
⊢ dropFun (toSubtype p) Fin2.fz x✝ = toSubtype (fun i x => p (Fin2.fs i) x) Fin2.fz x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec (n✝ + 1)} (p : α ⟹ repeat (n✝ + 1) Prop) (x : drop (fun i => { x // ofRepeat (p i x) }) a✝),
    dropFun (toSubtype p) a✝ x = toSubtype (fun i x => p (Fin2.fs i) x) a✝ x
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (fun i => { x // ofRepeat (p i x) }) (Fin2.fs a✝)
⊢ dropFun (toSubtype p) (Fin2.fs a✝) x✝ = toSubtype (fun i x => p (Fin2.fs i) x) (Fin2.fs a✝) x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (fun i => { x // ofRepeat (p i x) }) Fin2.fz
⊢ toSubtype p (Fin2.fs Fin2.fz) x✝ = toSubtype (fun i x => p (Fin2.fs i) x) Fin2.fz x✝
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec (n✝ + 1)} (p : α ⟹ repeat (n✝ + 1) Prop) (x : drop (fun i => { x // ofRepeat (p i x) }) a✝),
    dropFun (toSubtype p) a✝ x = toSubtype (fun i x => p (Fin2.fs i) x) a✝ x
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (fun i => { x // ofRepeat (p i x) }) (Fin2.fs a✝)
⊢ toSubtype p (Fin2.fs (Fin2.fs a✝)) x✝ = toSubtype (fun i x => p (Fin2.fs i) x) (Fin2.fs a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ lastFun (toSubtype p) = _root_.id
[PROOFSTEP]
ext i : 2
[GOAL]
case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last fun i => { x // ofRepeat (p i x) }
⊢ lastFun (toSubtype p) i = _root_.id i
[PROOFSTEP]
induction i
[GOAL]
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ dropFun (ofSubtype p) = ofSubtype (dropFun p)
[PROOFSTEP]
ext i : 2
[GOAL]
case a.h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : Fin2 n
x✝ : drop (Subtype_ p) i
⊢ dropFun (ofSubtype p) i x✝ = ofSubtype (dropFun p) i x✝
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (Subtype_ p) Fin2.fz
⊢ dropFun (ofSubtype p) Fin2.fz x✝ = ofSubtype (dropFun p) Fin2.fz x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec (n✝ + 1)} (p : α ⟹ repeat (n✝ + 1) Prop) (x : drop (Subtype_ p) a✝),
    dropFun (ofSubtype p) a✝ x = ofSubtype (dropFun p) a✝ x
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (Subtype_ p) (Fin2.fs a✝)
⊢ dropFun (ofSubtype p) (Fin2.fs a✝) x✝ = ofSubtype (dropFun p) (Fin2.fs a✝) x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (Subtype_ p) Fin2.fz
⊢ ofSubtype p (Fin2.fs Fin2.fz) x✝ = ofSubtype (fun i => p (Fin2.fs i)) Fin2.fz x✝
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec (n✝ + 1)} (p : α ⟹ repeat (n✝ + 1) Prop) (x : drop (Subtype_ p) a✝),
    dropFun (ofSubtype p) a✝ x = ofSubtype (dropFun p) a✝ x
α : TypeVec (Nat.succ n✝ + 1)
p : α ⟹ repeat (Nat.succ n✝ + 1) Prop
x✝ : drop (Subtype_ p) (Fin2.fs a✝)
⊢ ofSubtype p (Fin2.fs (Fin2.fs a✝)) x✝ = ofSubtype (fun i => p (Fin2.fs i)) (Fin2.fs a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ lastFun (ofSubtype p) = _root_.id
[PROOFSTEP]
ext i : 2
[GOAL]
case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last (Subtype_ p)
⊢ lastFun (ofSubtype p) i = _root_.id i
[PROOFSTEP]
induction i
[GOAL]
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ dropFun (f ⊗' f') = (dropFun f ⊗' dropFun f')
[PROOFSTEP]
ext i : 2
[GOAL]
case a.h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : Fin2 n
x✝ : drop (α ⊗ α') i
⊢ dropFun (f ⊗' f') i x✝ = (dropFun f ⊗' dropFun f') i x✝
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α α' β β' : TypeVec (Nat.succ n✝ + 1)
f : α ⟹ β
f' : α' ⟹ β'
x✝ : drop (α ⊗ α') Fin2.fz
⊢ dropFun (f ⊗' f') Fin2.fz x✝ = (dropFun f ⊗' dropFun f') Fin2.fz x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α α' β β' : TypeVec (n✝ + 1)} (f : α ⟹ β) (f' : α' ⟹ β') (x : drop (α ⊗ α') a✝),
    dropFun (f ⊗' f') a✝ x = (dropFun f ⊗' dropFun f') a✝ x
α α' β β' : TypeVec (Nat.succ n✝ + 1)
f : α ⟹ β
f' : α' ⟹ β'
x✝ : drop (α ⊗ α') (Fin2.fs a✝)
⊢ dropFun (f ⊗' f') (Fin2.fs a✝) x✝ = (dropFun f ⊗' dropFun f') (Fin2.fs a✝) x✝
[PROOFSTEP]
simp [dropFun, *]
[GOAL]
case a.h.fz
n n✝ : ℕ
α α' β β' : TypeVec (Nat.succ n✝ + 1)
f : α ⟹ β
f' : α' ⟹ β'
x✝ : drop (α ⊗ α') Fin2.fz
⊢ (f ⊗' f') (Fin2.fs Fin2.fz) x✝ = ((fun i => f (Fin2.fs i)) ⊗' fun i => f' (Fin2.fs i)) Fin2.fz x✝
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α α' β β' : TypeVec (n✝ + 1)} (f : α ⟹ β) (f' : α' ⟹ β') (x : drop (α ⊗ α') a✝),
    dropFun (f ⊗' f') a✝ x = (dropFun f ⊗' dropFun f') a✝ x
α α' β β' : TypeVec (Nat.succ n✝ + 1)
f : α ⟹ β
f' : α' ⟹ β'
x✝ : drop (α ⊗ α') (Fin2.fs a✝)
⊢ (f ⊗' f') (Fin2.fs (Fin2.fs a✝)) x✝ = ((fun i => f (Fin2.fs i)) ⊗' fun i => f' (Fin2.fs i)) (Fin2.fs a✝) x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ lastFun (f ⊗' f') = Prod.map (lastFun f) (lastFun f')
[PROOFSTEP]
ext i : 1
[GOAL]
case h
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : last (α ⊗ α')
⊢ lastFun (f ⊗' f') i = Prod.map (lastFun f) (lastFun f') i
[PROOFSTEP]
induction i
[GOAL]
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ lastFun (f ⊗' f') (fst✝, snd✝) = Prod.map (lastFun f) (lastFun f') (fst✝, snd✝)
[PROOFSTEP]
simp [lastFun, *]
[GOAL]
case h.mk
n : ℕ
α α' β β' : TypeVec (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : last α
snd✝ : last α'
⊢ (f ⊗' f') Fin2.fz (fst✝, snd✝) = Prod.map (f Fin2.fz) (f' Fin2.fz) (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α β : TypeVec n
⊢ (id ⊗' id) = id
[PROOFSTEP]
ext i x : 2
[GOAL]
case a.h
n : ℕ
α β : TypeVec n
i : Fin2 n
x : (α ⊗ β) i
⊢ (id ⊗' id) i x = id i x
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) Fin2.fz
⊢ (id ⊗' id) Fin2.fz x = id Fin2.fz x
[PROOFSTEP]
simp only [TypeVec.prod.map, *, dropFun_id]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ (id ⊗' id) (Fin2.fs a✝) x = id (Fin2.fs a✝) x
[PROOFSTEP]
simp only [TypeVec.prod.map, *, dropFun_id]
[GOAL]
case a.h.fz
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) Fin2.fz
⊢ (id Fin2.fz x.fst, id Fin2.fz x.snd) = id Fin2.fz x
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
[PROOFSTEP]
cases x
[GOAL]
case a.h.fz.mk
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
fst✝ : last α
snd✝ : last β
⊢ (id Fin2.fz (fst✝, snd✝).fst, id Fin2.fz (fst✝, snd✝).snd) = id Fin2.fz (fst✝, snd✝)
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
[PROOFSTEP]
rfl
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : TypeVec n
⊢ subtypeVal (repeatEq α) ⊚ diagSub = prod.diag
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) i x = prod.diag i x
[PROOFSTEP]
induction' i with _ _ _ i_ih
[GOAL]
case a.h.fz
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
α : TypeVec (Nat.succ n✝)
x : α Fin2.fz
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x
[PROOFSTEP]
simp [comp, diagSub, subtypeVal, prod.diag]
[GOAL]
case a.h.fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (Nat.succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
[PROOFSTEP]
simp [prod.diag]
[GOAL]
case a.h.fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (Nat.succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag a✝ x
[PROOFSTEP]
simp [comp, diagSub, subtypeVal, prod.diag] at *
[GOAL]
case a.h.fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), subtypeVal (repeatEq α) a✝ (diagSub a✝ x) = prod.diag a✝ x
α : TypeVec (Nat.succ n✝)
x : α (Fin2.fs a✝)
⊢ subtypeVal (dropFun (repeatEq α)) a✝ (diagSub a✝ x) = prod.diag a✝ x
[PROOFSTEP]
apply @i_ih (drop _)
[GOAL]
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
⊢ toSubtype p ⊚ ofSubtype p = id
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ p Fin2.fz
⊢ (toSubtype p ⊚ ofSubtype p) Fin2.fz x = id Fin2.fz x
[PROOFSTEP]
dsimp only [id, toSubtype, comp, ofSubtype] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : Subtype_ p a✝), (toSubtype p ⊚ ofSubtype p) a✝ x = id a✝ x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ p (Fin2.fs a✝)
⊢ (toSubtype p ⊚ ofSubtype p) (Fin2.fs a✝) x = id (Fin2.fs a✝) x
[PROOFSTEP]
dsimp only [id, toSubtype, comp, ofSubtype] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ p (Fin2.fs a✝)
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x
[PROOFSTEP]
simp [*]
[GOAL]
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x => Subtype.val
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (p Fin2.fz x) }
⊢ (subtypeVal p ⊚ toSubtype p) Fin2.fz x = ↑x
[PROOFSTEP]
dsimp only [toSubtype, comp, subtypeVal] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : (fun i => { x // ofRepeat (p i x) }) a✝),
    (subtypeVal p ⊚ toSubtype p) a✝ x = ↑x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (p (Fin2.fs a✝) x) }
⊢ (subtypeVal p ⊚ toSubtype p) (Fin2.fs a✝) x = ↑x
[PROOFSTEP]
dsimp only [toSubtype, comp, subtypeVal] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (p a✝ x) }), subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (p (Fin2.fs a✝) x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x
[PROOFSTEP]
simp [*]
[GOAL]
n : ℕ
α : TypeVec n
β : TypeVec n
p : α ⟹ repeat n Prop
f : β ⟹ Subtype_ p
⊢ toSubtype p ⊚ (ofSubtype fun i x => p i x) ⊚ f = f
[PROOFSTEP]
rw [← comp_assoc, toSubtype_of_subtype]
[GOAL]
n : ℕ
α : TypeVec n
β : TypeVec n
p : α ⟹ repeat n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
⊢ toSubtype' r ⊚ ofSubtype' r = id
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : Subtype_ r i
⊢ (toSubtype' r ⊚ ofSubtype' r) i x = id i x
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ r Fin2.fz
⊢ (toSubtype' r ⊚ ofSubtype' r) Fin2.fz x = id Fin2.fz x
[PROOFSTEP]
dsimp only [id, toSubtype', comp, ofSubtype'] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : Subtype_ r a✝), (toSubtype' r ⊚ ofSubtype' r) a✝ x = id a✝ x
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ r (Fin2.fs a✝)
⊢ (toSubtype' r ⊚ ofSubtype' r) (Fin2.fs a✝) x = id (Fin2.fs a✝) x
[PROOFSTEP]
dsimp only [id, toSubtype', comp, ofSubtype'] at *
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ r Fin2.fz
⊢ { val := ↑x,
      property :=
        (_ : r Fin2.fz ↑{ val := ↑x, property := (_ : ofRepeat (r Fin2.fz (prod.mk Fin2.fz (↑x).fst (↑x).snd))) }) } =
    x
[PROOFSTEP]
simp [Subtype.eta, *]
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : Subtype_ r (Fin2.fs a✝)
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x
[PROOFSTEP]
simp [Subtype.eta, *]
[GOAL]
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i (↑x).fst (↑x).snd
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
α : TypeVec n
r : α ⊗ α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (r i (prod.mk i x.fst x.snd)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).fst (↑x).snd
[PROOFSTEP]
induction i
[GOAL]
case a.h.fz
n n✝ : ℕ
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (r Fin2.fz (prod.mk Fin2.fz x.fst x.snd)) }
⊢ (subtypeVal r ⊚ toSubtype' r) Fin2.fz x = prod.mk Fin2.fz (↑x).fst (↑x).snd
[PROOFSTEP]
dsimp only [id, toSubtype', comp, subtypeVal, prod.mk] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : (fun i => { x // ofRepeat (r i (prod.mk i x.fst x.snd)) }) a✝),
    (subtypeVal r ⊚ toSubtype' r) a✝ x = prod.mk a✝ (↑x).fst (↑x).snd
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (r (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd)) }
⊢ (subtypeVal r ⊚ toSubtype' r) (Fin2.fs a✝) x = prod.mk (Fin2.fs a✝) (↑x).fst (↑x).snd
[PROOFSTEP]
dsimp only [id, toSubtype', comp, subtypeVal, prod.mk] at *
[GOAL]
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (r : α ⊗ α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.fst x.snd)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
α : TypeVec (Nat.succ n✝)
r : α ⊗ α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (r (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x.fst x.snd)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).fst (↑x).snd
[PROOFSTEP]
simp [*]
