[GOAL]
α : Type u
x : Tree α
⊢ numLeaves x = numNodes x + 1
[PROOFSTEP]
induction x
[GOAL]
case nil
α : Type u
⊢ numLeaves nil = numNodes nil + 1
[PROOFSTEP]
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
[GOAL]
case node
α : Type u
a✝² : α
a✝¹ a✝ : Tree α
a_ih✝¹ : numLeaves a✝¹ = numNodes a✝¹ + 1
a_ih✝ : numLeaves a✝ = numNodes a✝ + 1
⊢ numLeaves (node a✝² a✝¹ a✝) = numNodes (node a✝² a✝¹ a✝) + 1
[PROOFSTEP]
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
[GOAL]
α : Type u
x : Tree α
⊢ 0 < numLeaves x
[PROOFSTEP]
rw [numLeaves_eq_numNodes_succ]
[GOAL]
α : Type u
x : Tree α
⊢ 0 < numNodes x + 1
[PROOFSTEP]
exact x.numNodes.zero_lt_succ
[GOAL]
α : Type u
h : nil ≠ nil
⊢ node () (left nil) (right nil) = nil
[PROOFSTEP]
trivial


[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 [*]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ Option.isSome (toOption o) = true ↔ o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ Option.isNone (toOption o) = true ↔ ¬o.Dom
[PROOFSTEP]
simp [h, toOption]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
[PROOFSTEP]
have t : od = pd := propext H1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := pd, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := pd, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := pd, get := p } h₂
t : od = pd
⊢ { Dom := od, get := o } = { Dom := pd, get := p }
[PROOFSTEP]
cases t
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    get { Dom := od, get := o } h₁ = get { Dom := od, get := p } h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }
[PROOFSTEP]
rw [show o = p from funext fun p => H2 p p]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : ∀ (a : α), ¬a ∈ o
⊢ ∀ (a : α), a ∈ o ↔ a ∈ none
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ some x ≠ none
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
h : some x = none
⊢ False
[PROOFSTEP]
exact true_ne_false (congr_arg Dom h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o ≠ none ↔ ∃ x, o = some x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o ≠ none → ∃ x, o = some x
[PROOFSTEP]
rw [Ne, eq_none_iff', not_not]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ o.Dom → ∃ x, o = some x
[PROOFSTEP]
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
⊢ (∃ x, o = some x) → o ≠ none
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : α
⊢ some x ≠ none
[PROOFSTEP]
apply some_ne_none
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : α
h : get a ha = b
⊢ a = some b
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : α
h : a = some b
⊢ get a ha = b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
ha : a.Dom
b : Part α
h : a = b
⊢ get a ha = get b (_ : b.Dom)
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ a ∈ toOption o ↔ a ∈ o
[PROOFSTEP]
unfold toOption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (get o h) else Option.none) ↔ a ∈ o
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ get o (_ : o.Dom) = a ↔ a ∈ o
[PROOFSTEP]
exact ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o
[PROOFSTEP]
exact mt Exists.fst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ toOption o = Option.some a ↔ a ∈ o
[PROOFSTEP]
rw [← Option.mem_def, mem_toOption]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ Option.elim (toOption a) b f = if h : a.Dom then f (get a h) else b
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (toOption a) b f = f (get a h)
[PROOFSTEP]
rw [h.toOption]
[GOAL]
case pos
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ Option.elim (Option.some (get a h)) b f = f (get a h)
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim (toOption a) b f = b
[PROOFSTEP]
rw [Part.toOption_eq_none_iff.2 h]
[GOAL]
case neg
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim Option.none b f = b
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ (↑Option.none).Dom ↔ Option.isSome Option.none = true
[PROOFSTEP]
simp [ofOption, none]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ Option.isSome (Option.some a) = true
[PROOFSTEP]
simp [ofOption]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := Option.isSome o = true, get := Option.get o }.Dom
⊢ get (↑o) h₁ = get { Dom := Option.isSome o = true, get := Option.get o } h₂
[PROOFSTEP]
cases o
[GOAL]
case none
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.isSome Option.none = true, get := Option.get Option.none }.Dom
⊢ get (↑Option.none) h₁ = get { Dom := Option.isSome Option.none = true, get := Option.get Option.none } h₂
[PROOFSTEP]
simp at h₂
[GOAL]
case some
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) }.Dom
⊢ get (↑(Option.some val✝)) h₁ =
    get { Dom := Option.isSome (Option.some val✝) = true, get := Option.get (Option.some val✝) } h₂
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Option α
⊢ toOption ↑o = o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ toOption ↑Option.none = Option.none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
γ : Type u_3
val✝ : α
⊢ toOption ↑(Option.some val✝) = Option.some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o => toOption o) ↑o = toOption ↑o
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ toOption ↑o = toOption ↑o
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ (a : Part α), ⊥ ≤ a
[PROOFSTEP]
introv x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : Part α
x : α
⊢ x ∈ ⊥ → x ∈ a
[PROOFSTEP]
rintro ⟨⟨_⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
rw [h]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
[PROOFSTEP]
left
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y
[PROOFSTEP]
apply OrderBot.bot_le _
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
right
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
[PROOFSTEP]
intro b' h₁
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
[PROOFSTEP]
rw [Part.eq_some_iff] at h₀
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
[PROOFSTEP]
have hx := hx _ h₀
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
[PROOFSTEP]
have hy := hy _ h₁
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b' ∈ x
[PROOFSTEP]
have hx := Part.mem_unique hx hy
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝¹ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx✝ : b ∈ z
hy : b' ∈ z
hx : b = b'
⊢ b' ∈ x
[PROOFSTEP]
subst hx
[GOAL]
case inr.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : Part α
hx✝ : x ≤ z
hy✝ : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x
[PROOFSTEP]
exact h₀
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a : β
⊢ ¬a ∈ map f none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h
[PROOFSTEP]
dsimp [assert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = f h
[PROOFSTEP]
cases h' : f h
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = { Dom := Dom✝, get := get✝ }
[PROOFSTEP]
simp [h', mk.injEq, h, exists_prop_of_true, true_and]
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) get✝
[PROOFSTEP]
apply Function.hfunext
[GOAL]
case mk.hα
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ h, (f h).Dom) = Dom✝
[PROOFSTEP]
simp only [h, h', exists_prop_of_true]
[GOAL]
case mk.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) (get✝ a')
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none
[PROOFSTEP]
dsimp [assert, none]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }
[PROOFSTEP]
congr
[GOAL]
case h.e_2
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
[PROOFSTEP]
simp only [h, not_false_iff, exists_prop_of_false]
[GOAL]
case h.e_3
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom)) fun t => False.rec (fun x => α) t
[PROOFSTEP]
apply Function.hfunext
[GOAL]
case h.e_3.hα
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
[PROOFSTEP]
simp only [h, not_false_iff, exists_prop_of_false]
[GOAL]
case h.e_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : False),
    HEq a a' → HEq (get (f (_ : p)) (_ : (f (_ : p)).Dom)) (False.rec (fun x => α) a')
[PROOFSTEP]
simp at *
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
⊢ Part.bind o f = f (get o h)
[PROOFSTEP]
ext b
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ Part.bind o f ↔ b ∈ f (get o h)
[PROOFSTEP]
simp only [Part.mem_bind_iff, exists_prop]
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) ↔ b ∈ f (get o h)
[PROOFSTEP]
refine' ⟨_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (get o h)
[PROOFSTEP]
rintro ⟨a, ha, hb⟩
[GOAL]
case H.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (get o h)
[PROOFSTEP]
rwa [Part.get_eq_of_mem ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
a : β
⊢ ¬a ∈ Part.bind none f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ Part.bind (some a) f ↔ a_1 ∈ f a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ Part.bind o f = f a
[PROOFSTEP]
rw [eq_some_iff.2 h, bind_some]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x : Part α
⊢ ∀ (a : β), a ∈ Part.bind x (some ∘ f) ↔ a ∈ map f x
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
by_cases h : o.Dom
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
simp_rw [h.toOption, h.bind]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : o.Dom
⊢ toOption (f (get o h)) = Option.elim (Option.some (get o h)) Option.none fun a => toOption (f a)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim (toOption o) Option.none fun a => toOption (f a)
[PROOFSTEP]
rw [Part.toOption_eq_none_iff.2 h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (Part.bind o f).Dom
h : ¬o.Dom
⊢ toOption (Part.bind o f) = Option.elim Option.none Option.none fun a => toOption (f a)
[PROOFSTEP]
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ Part.bind (Part.bind f g) k ↔ a ∈ Part.bind f fun x => Part.bind (g x) k
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ a_1, (∃ a, a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1, a_1 ∈ f ∧ ∃ a_2, a_2 ∈ g a_1 ∧ a ∈ k a_2
[PROOFSTEP]
exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩, fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ Part.bind (map f x) g = Part.bind x fun y => g (f y)
[PROOFSTEP]
rw [← bind_some_eq_map, bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ (Part.bind x fun x => Part.bind ((some ∘ f) x) g) = Part.bind x fun y => g (f y)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (Part.bind x f) = Part.bind x fun y => map g (f y)
[PROOFSTEP]
rw [← bind_some_eq_map, bind_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (Part.bind x fun x => Part.bind (f x) (some ∘ g)) = Part.bind x fun y => map g (f y)
[PROOFSTEP]
simp [bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o
[PROOFSTEP]
erw [← bind_some_eq_map, bind_map, bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type ?u.35509}, Functor.mapConst = Functor.map ∘ const β
[PROOFSTEP]
simp [Functor.mapConst, Functor.map]
  --Porting TODO : In Lean3 these were automatic by a tactic
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type ?u.35509
f : Part α✝
⊢ id <$> f = f
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ : Type ?u.35509
Dom✝ : Prop
get✝ : Dom✝ → α✝
⊢ id <$> { Dom := Dom✝, get := get✝ } = { Dom := Dom✝, get := get✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part α✝
y : Part β✝
⊢ (SeqLeft.seqLeft x fun x => y).Dom ↔ (Seq.seq (const β✝ <$> x) fun x => y).Dom
[PROOFSTEP]
simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part α✝
y : Part β✝
⊢ (SeqRight.seqRight x fun x => y).Dom ↔ (Seq.seq (const α✝ id <$> x) fun x => y).Dom
[PROOFSTEP]
simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : α✝ → β✝
y : Part α✝
⊢ (Seq.seq (pure x) fun x => y).Dom ↔ (x <$> y).Dom
[PROOFSTEP]
simp [Seq.seq, Part.bind, assert, (· <$> ·), pure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
α✝ β✝ : Type ?u.35509
x : Part (α✝ → β✝)
y : Part α✝
⊢ (do
        let x ← x
        x <$> y).Dom ↔
    (Seq.seq x fun x => y).Dom
[PROOFSTEP]
simp [(· >>= ·), Part.bind, assert, Seq.seq, get, (· <$> ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o
[PROOFSTEP]
rw [show f = id from funext H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o
[PROOFSTEP]
exact id_map o
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Part α
⊢ Part.bind x some = x
[PROOFSTEP]
erw [bind_some_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : Part α
⊢ map (fun a => a) x = x
[PROOFSTEP]
simp [map_id']
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y
[PROOFSTEP]
intro a h' b
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
have h := h b
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp] at h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y
[PROOFSTEP]
apply h _ h'
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y
[PROOFSTEP]
intro b h'
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
[PROOFSTEP]
simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h'
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ a, a ∈ x ∧ b ∈ f a
⊢ b ∈ y
[PROOFSTEP]
rcases h' with ⟨a, h₀, h₁⟩
[GOAL]
case mpr.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y
[PROOFSTEP]
apply h _ h₀ _ h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o
[PROOFSTEP]
dsimp [restrict, mem_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) ↔ p ∧ ∃ h, get o h = a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ h_1, get o (_ : o.Dom) = a) → p ∧ ∃ h, get o h = a
[PROOFSTEP]
rintro ⟨h₀, h₁⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : get o (_ : o.Dom) = a
⊢ p ∧ ∃ h, get o h = a
[PROOFSTEP]
exact ⟨h₀, ⟨_, h₁⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ h, get o h = a) → ∃ h_1, get o (_ : o.Dom) = a
[PROOFSTEP]
rintro ⟨h₀, _, h₂⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : get o w✝ = a
⊢ ∃ h_1, get o (_ : o.Dom) = a
[PROOFSTEP]
exact ⟨h₀, h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    ma * mb
[PROOFSTEP]
simp [← ha.2, ← hb.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ get (a * b)
      (_ : ∃ h, ((fun b_1 => (fun y => map y ((fun x => b) ())) (get ((fun x x_1 => x * x_1) <$> a) b_1)) h).Dom) =
    get a (_ : a.Dom) * get b (_ : b.Dom)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul α
a b : α
⊢ some a * some b = some (a * b)
[PROOFSTEP]
simp [mul_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹
[PROOFSTEP]
simp [inv_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1, a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 / a = ma / mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ get (a / b) hab = get a (_ : a.Dom) / get b (_ : b.Dom)
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : Part α
hab : (a / b).Dom
⊢ get (Part.bind a fun y => map (fun x => y / x) b) (_ : (Part.bind a fun y => map (fun x => y / x) b).Dom) =
    get a (_ : a.Dom) / get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Div α
a b : α
⊢ some a / some b = some (a / b)
[PROOFSTEP]
simp [div_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 % a = ma % mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ get (a % b) hab = get a (_ : a.Dom) % get b (_ : b.Dom)
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : Part α
hab : (a % b).Dom
⊢ get (Part.bind a fun y => map (fun x => y % x) b) (_ : (Part.bind a fun y => map (fun x => y % x) b).Dom) =
    get a (_ : a.Dom) % get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mod α
a b : α
⊢ some a % some b = some (a % b)
[PROOFSTEP]
simp [mod_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ++ a = ma ++ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ get (a ++ b) hab = get a (_ : a.Dom) ++ get b (_ : b.Dom)
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ++ x) b) (_ : (Part.bind a fun y => map (fun x => y ++ x) b).Dom) =
    get a (_ : a.Dom) ++ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Append α
a b : α
⊢ some a ++ some b = some (a ++ b)
[PROOFSTEP]
simp [append_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∩ mb ∈ a ∩ b
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∩ a = ma ∩ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ get (a ∩ b) hab = get a (_ : a.Dom) ∩ get b (_ : b.Dom)
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∩ x) b) (_ : (Part.bind a fun y => map (fun x => y ∩ x) b).Dom) =
    get a (_ : a.Dom) ∩ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)
[PROOFSTEP]
simp [inter_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ∪ a = ma ∪ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (a ∪ b) hab = get a (_ : a.Dom) ∪ get b (_ : b.Dom)
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y ∪ x) b) (_ : (Part.bind a fun y => map (fun x => y ∪ x) b).Dom) =
    get a (_ : a.Dom) ∪ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)
[PROOFSTEP]
simp [union_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma \ mb ∈ a \ b
[PROOFSTEP]
simp [sdiff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 \ a = ma \ mb
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ get (a \ b) hab = get a (_ : a.Dom) \ get b (_ : b.Dom)
[PROOFSTEP]
simp [sdiff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ get (Part.bind a fun y => map (fun x => y \ x) b) (_ : (Part.bind a fun y => map (fun x => y \ x) b).Dom) =
    get a (_ : a.Dom) \ get b (_ : b.Dom)
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)
[PROOFSTEP]
simp [sdiff_def]