[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec n} (x : Sigma F α), (fun {α} => Sigma.abs F) ((fun {α} => Sigma.repr F) x) = x
[PROOFSTEP]
rintro α ⟨x, f⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec n
x : A
f : F x α
⊢ (fun {α} => Sigma.abs F) ((fun {α} => Sigma.repr F) { fst := x, snd := f }) = { fst := x, snd := f }
[PROOFSTEP]
simp only [Sigma.abs, Sigma.repr, Sigma.eta, abs_repr]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (Sigma.P F) α),
    (fun {α} => Sigma.abs F) (f <$$> p) = f <$$> (fun {α} => Sigma.abs F) p
[PROOFSTEP]
rintro α β f ⟨x, g⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Sigma.P F).A
g : MvPFunctor.B (Sigma.P F) x ⟹ α
⊢ (fun {α} => Sigma.abs F) (f <$$> { fst := x, snd := g }) = f <$$> (fun {α} => Sigma.abs F) { fst := x, snd := g }
[PROOFSTEP]
simp only [Sigma.abs, MvPFunctor.map_eq]
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Sigma.P F).A
g : MvPFunctor.B (Sigma.P F) x ⟹ α
⊢ { fst := x.fst, snd := abs { fst := x.snd, snd := f ⊚ g } } =
    f <$$> { fst := x.fst, snd := abs { fst := x.snd, snd := g } }
[PROOFSTEP]
simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α : TypeVec n} (x : Pi F α), Pi.abs F (Pi.repr F x) = x
[PROOFSTEP]
rintro α f
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α : TypeVec n
f : Pi F α
⊢ Pi.abs F (Pi.repr F f) = f
[PROOFSTEP]
simp only [Pi.abs, Pi.repr, Sigma.eta, abs_repr]
[GOAL]
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (Pi.P F) α), Pi.abs F (f <$$> p) = f <$$> Pi.abs F p
[PROOFSTEP]
rintro α β f ⟨x, g⟩
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Pi.P F).A
g : MvPFunctor.B (Pi.P F) x ⟹ α
⊢ Pi.abs F (f <$$> { fst := x, snd := g }) = f <$$> Pi.abs F { fst := x, snd := g }
[PROOFSTEP]
simp only [Pi.abs, (· <$$> ·), ← abs_map]
[GOAL]
case mk
n : ℕ
A : Type u
F : A → TypeVec n → Type u
inst✝¹ : (α : A) → MvFunctor (F α)
inst✝ : (α : A) → MvQPF (F α)
α β : TypeVec n
f : α ⟹ β
x : (Pi.P F).A
g : MvPFunctor.B (Pi.P F) x ⟹ α
⊢ (match MvPFunctor.map (Pi.P F) f { fst := x, snd := g } with
    | { fst := a, snd := f } => fun x => abs { fst := a x, snd := fun i y => f i { fst := x, snd := y } }) =
    fun a => abs (MvPFunctor.map (P (F a)) f { fst := x a, snd := fun i y => g i { fst := a, snd := y } })
[PROOFSTEP]
rfl


[GOAL]
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ Nodup (keys m) ↔ NodupKeys m
[PROOFSTEP]
rcases m with ⟨l⟩
[GOAL]
case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ Nodup (keys (Quot.mk Setoid.r l)) ↔ NodupKeys (Quot.mk Setoid.r l)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries
[PROOFSTEP]
cases s₁
[GOAL]
case mk
α : Type u
β : α → Type v
s₂ : AList β
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ = ⟦s₂⟧ ↔
    { entries := entries✝, nodupKeys := nodupKeys✝ }.entries ~ s₂.entries
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
α : Type u
β : α → Type v
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ = ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ↔
    { entries := entries✝¹, nodupKeys := nodupKeys✝¹ }.entries ~
      { entries := entries✝, nodupKeys := nodupKeys✝ }.entries
[PROOFSTEP]
simp [AList.toFinmap]
[GOAL]
α : Type u
β : α → Type v
γ : Sort ?u.11051
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ γ
[PROOFSTEP]
refine'
  (Quotient.liftOn s.entries (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
          (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) _) :
        Part γ).get
    _
[GOAL]
case refine'_1
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀ (h₁ : ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁).Dom)
    (h₂ : ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂).Dom),
    Part.get ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁) h₁ =
      Part.get ((fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂) h₂
[PROOFSTEP]
exact fun h1 h2 => H _ _ p
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
      (_ :
        ∀ (l₁ l₂ : List (Sigma β)),
          l₁ ≈ l₂ →
            (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
have := s.nodupKeys
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
this : Multiset.NodupKeys s.entries
⊢ (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
      (_ :
        ∀ (l₁ l₂ : List (Sigma β)),
          l₁ ≈ l₂ →
            (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
revert this
[GOAL]
case refine'_2
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ Multiset.NodupKeys s.entries →
    (Quotient.liftOn s.entries (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
        (_ :
          ∀ (l₁ l₂ : List (Sigma β)),
            l₁ ≈ l₂ →
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
                (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
rcases s.entries with ⟨l⟩
[GOAL]
case refine'_2.mk
α : Type u
β : α → Type v
γ : Type ?u.11103
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
x✝ : Multiset (Sigma β)
l : List (Sigma β)
⊢ Multiset.NodupKeys (Quot.mk Setoid.r l) →
    (Quotient.liftOn (Quot.mk Setoid.r l)
        (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } })
        (_ :
          ∀ (l₁ l₂ : List (Sigma β)),
            l₁ ≈ l₂ →
              (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₁ =
                (fun l => { Dom := NodupKeys l, get := fun nd => f { entries := l, nodupKeys := nd } }) l₂)).Dom
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ liftOn ⟦s⟧ f H = f s
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H = f { entries := entries✝, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
γ : Type ?u.20104
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
⊢ (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₁ =
    (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₂
[PROOFSTEP]
have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)
[GOAL]
α : Type u
β : α → Type v
γ : Type ?u.20104
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
H' : f a₁ = f a₂
⊢ (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₁ =
    (fun l₁ => liftOn s₂ (f l₁) (_ : ∀ (b₁ b₂ : AList β), b₁.entries ~ b₂.entries → f l₁ b₁ = f l₁ b₂)) a₂
[PROOFSTEP]
simp only [H']
[GOAL]
α : Type u
β : α → Type v
γ : Type u_1
s₁ s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
⊢ liftOn₂ ⟦s₁⟧ ⟦s₂⟧ f H = f s₁ s₂
[PROOFSTEP]
cases s₁
[GOAL]
case mk
α : Type u
β : α → Type v
γ : Type u_1
s₂ : AList β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ ⟦s₂⟧ f H =
    f { entries := entries✝, nodupKeys := nodupKeys✝ } s₂
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
α : Type u
β : α → Type v
γ : Type u_1
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
entries✝¹ : List (Sigma β)
nodupKeys✝¹ : NodupKeys entries✝¹
entries✝ : List (Sigma β)
nodupKeys✝ : NodupKeys entries✝
⊢ liftOn₂ ⟦{ entries := entries✝¹, nodupKeys := nodupKeys✝¹ }⟧ ⟦{ entries := entries✝, nodupKeys := nodupKeys✝ }⟧ f H =
    f { entries := entries✝¹, nodupKeys := nodupKeys✝¹ } { entries := entries✝, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s
[PROOFSTEP]
rcases s with ⟨⟨a⟩, h⟩
[GOAL]
case mk.mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk Setoid.r a)
⊢ C { entries := Quot.mk Setoid.r a, nodupKeys := h }
[PROOFSTEP]
exact H ⟨a, h⟩
[GOAL]
α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : Multiset.NodupKeys l₁
l₂ : Multiset (Sigma β)
nodupKeys✝ : Multiset.NodupKeys l₂
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ keys ⟦s₁⟧ = keys ⟦s₂⟧ ↔ AList.keys s₁ ~ AList.keys s₂
[PROOFSTEP]
simp [keys, AList.keys]
[GOAL]
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y
[PROOFSTEP]
simp only [singleton]
[GOAL]
α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ ⟦AList.singleton y b⟧ ↔ x = y
[PROOFSTEP]
erw [mem_cons, mem_nil_iff, or_false_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a (List.toFinmap s) = dlookup a s
[PROOFSTEP]
rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup a s ↔ { fst := a, snd := b } ∈ s.entries
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk Setoid.r l)
⊢ b ∈ lookup a { entries := Quot.mk Setoid.r l, nodupKeys := hl } ↔
    { fst := a, snd := b } ∈ { entries := Quot.mk Setoid.r l, nodupKeys := hl }.entries
[PROOFSTEP]
exact List.mem_dlookup_iff hl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) =
    { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ (x ∈ Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) ↔
    x ∈ { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries → x.fst ∈ keys s
⊢ (x ∈ Finset.sigma (keys s) fun i => Option.toFinset (lookup i s)) ↔
    x ∈ { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
[PROOFSTEP]
simpa [lookup_eq_some_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a (singleton a b) = some b
[PROOFSTEP]
rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧
[PROOFSTEP]
simp only [AList.lookup, lookup_toFinmap] at h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ⟦s₁⟧ = ⟦s₂⟧
[PROOFSTEP]
rw [AList.toFinmap_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries
[PROOFSTEP]
apply lookup_ext s₁.nodupKeys s₂.nodupKeys
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
[PROOFSTEP]
intro x y
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
y : β x
⊢ y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val
[PROOFSTEP]
refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ ∀ (x : (a : α) × β a),
    x ∈ (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val →
      ∀ (y : (a : α) × β a),
        y ∈ (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val → x.fst = y.fst → x = y
[PROOFSTEP]
simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
⊢ ∀ (x : (a : α) × β a),
    x.fst ∈ (↑f).fst ∧ Prod.snd (↑f) x.fst = some x.snd →
      ∀ (y : (a : α) × β a), y.fst ∈ (↑f).fst ∧ Prod.snd (↑f) y.fst = some y.snd → x.fst = y.fst → x = y
[PROOFSTEP]
rintro ⟨i, x⟩ ⟨_, hx⟩ ⟨j, y⟩ ⟨_, hy⟩ (rfl : i = j)
[GOAL]
case mk.intro.mk.intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
i : α
x : β i
left✝¹ : { fst := i, snd := x }.fst ∈ (↑f).fst
hx : Prod.snd ↑f { fst := i, snd := x }.fst = some { fst := i, snd := x }.snd
y : β i
left✝ : { fst := i, snd := y }.fst ∈ (↑f).fst
hy : Prod.snd ↑f { fst := i, snd := y }.fst = some { fst := i, snd := y }.snd
⊢ { fst := i, snd := x } = { fst := i, snd := y }
[PROOFSTEP]
simpa using hx.symm.trans hy
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : Finmap β
⊢ ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        ((fun s =>
            { val := (keys s, fun i => lookup i s),
              property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
          f)).entries =
    f.entries
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (Prod.snd (s, f) i) = true ↔ i ∈ (s, f).fst
⊢ (fun s =>
        { val := (keys s, fun i => lookup i s),
          property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
      ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        { val := (s, f), property := hf }) =
    { val := (s, f), property := hf }
[PROOFSTEP]
dsimp only at hf
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
⊢ (fun s =>
        { val := (keys s, fun i => lookup i s),
          property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
      ((fun f =>
          { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
            nodupKeys :=
              (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
        { val := (s, f), property := hf }) =
    { val := (s, f), property := hf }
[PROOFSTEP]
ext
[GOAL]
case a.h₁.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
a✝ : α
⊢ a✝ ∈
      (↑((fun s =>
              { val := (keys s, fun i => lookup i s),
                property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
            ((fun f =>
                { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
                  nodupKeys :=
                    (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
              { val := (s, f), property := hf }))).fst ↔
    a✝ ∈ (↑{ val := (s, f), property := hf }).fst
[PROOFSTEP]
simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]
[GOAL]
case a.h₂.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true ↔ i ∈ f.fst }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), Option.isSome (f i) = true ↔ i ∈ s
x✝ : α
a✝ : β x✝
⊢ a✝ ∈
      Prod.snd
        (↑((fun s =>
              { val := (keys s, fun i => lookup i s),
                property := (_ : ∀ (x : α), Option.isSome (lookup x s) = true ↔ x ∈ s) })
            ((fun f =>
                { entries := (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val,
                  nodupKeys :=
                    (_ : Multiset.NodupKeys (Finset.sigma (↑f).fst fun i => Option.toFinset (Prod.snd (↑f) i)).val) })
              { val := (s, f), property := hf })))
        x✝ ↔
    a✝ ∈ Prod.snd (↑{ val := (s, f), property := hf }) x✝
[PROOFSTEP]
simp (config := { contextual := true }) [lookup_eq_some_iff, ← hf]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : Finmap fun a => β a
⊢ keys (↑keysLookupEquiv.symm (↑keysLookupEquiv x✝)) = (↑(↑keysLookupEquiv x✝)).fst
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : Finmap fun a => β a
x✝ : α
⊢ lookup x✝ (↑keysLookupEquiv.symm (↑keysLookupEquiv x✝¹)) = Prod.snd (↑(↑keysLookupEquiv x✝¹)) x✝
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_snd]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧
[PROOFSTEP]
simp [replace]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ keys (replace a b ⟦s⟧) = keys ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝),
    (fun x y z => x || f y z) ((fun x y z => x || f y z) x✝³ x✝² x✝¹) x✝ b₂ =
      (fun x y z => x || f y z) ((fun x y z => x || f y z) x✝³ x✝ b₂) x✝² x✝¹
[PROOFSTEP]
simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]
[GOAL]
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝),
    (fun x y z => x && f y z) ((fun x y z => x && f y z) x✝³ x✝² x✝¹) x✝ b₂ =
      (fun x y z => x && f y z) ((fun x y z => x && f y z) x✝³ x✝ b₂) x✝² x✝¹
[PROOFSTEP]
simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ erase a ⟦s⟧ = ⟦AList.erase a s⟧
[PROOFSTEP]
simp [erase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ keys ⟦AList.erase a s⟧ = Finset.erase (keys ⟦s⟧) a
[PROOFSTEP]
simp [Finset.erase, keys, AList.erase, keys_kerase]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ keys (erase a ⟦s⟧) = Finset.erase (keys ⟦s⟧) a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ ¬a ∈ erase a s
[PROOFSTEP]
rw [mem_erase, not_and_or, not_not]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ ¬a ∈ s
[PROOFSTEP]
left
[GOAL]
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries
[PROOFSTEP]
simp only [AList.erase_erase, erase_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert a b ⟦s⟧ = ⟦AList.insert a b s⟧
[PROOFSTEP]
simp [insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
h : ¬a ∈ ⟦s⟧
⊢ (insert a b ⟦s⟧).entries = { fst := a, snd := b } ::ₘ ⟦s⟧.entries
[PROOFSTEP]
simp [AList.insert_entries_of_neg (mt mem_toFinmap.1 h), -insert_entries]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ lookup a (insert a b ⟦s⟧) = some b
[PROOFSTEP]
simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
h : a' ≠ a
s : AList β
⊢ lookup a' (insert a b ⟦s⟧) = lookup a' ⟦s⟧
[PROOFSTEP]
simp only [insert_toFinmap, lookup_toFinmap, lookup_insert_ne h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s✝ : Finmap β
s : AList β
⊢ insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧
[PROOFSTEP]
simp only [insert_toFinmap, AList.insert_insert]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s✝ : Finmap β
h : a ≠ a'
s : AList β
⊢ insert a' b' (insert a b ⟦s⟧) = insert a b (insert a' b' ⟦s⟧)
[PROOFSTEP]
simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
[PROOFSTEP]
induction' xs with x xs
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ List.toFinmap [] ↔ ∃ b, { fst := a, snd := b } ∈ []
[PROOFSTEP]
simp only [toFinmap_nil, not_mem_empty, find?, not_mem_nil, exists_false]
[GOAL]
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
⊢ a ∈ List.toFinmap (x :: xs) ↔ ∃ b, { fst := a, snd := b } ∈ x :: xs
[PROOFSTEP]
cases' x with fst_i snd_i
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ List.toFinmap ({ fst := fst_i, snd := snd_i } :: xs) ↔
    ∃ b, { fst := a, snd := b } ∈ { fst := fst_i, snd := snd_i } :: xs
[PROOFSTEP]
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, { fst := a, snd := b } ∈ xs) ↔ (a = fst_i ∧ ∃ x, HEq x snd_i) ∨ ∃ x, { fst := a, snd := x } ∈ xs
[PROOFSTEP]
refine (or_congr_left <| and_iff_left_of_imp ?_).symm
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a = fst_i → ∃ x, HEq x snd_i
[PROOFSTEP]
rintro rfl
[GOAL]
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ List.toFinmap xs ↔ ∃ b, { fst := a, snd := b } ∈ xs
snd_i : β a
⊢ ∃ x, HEq x snd_i
[PROOFSTEP]
simp only [exists_eq, heq_iff_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ insert a b (singleton a b') = singleton a b
[PROOFSTEP]
simp only [singleton, Finmap.insert_toFinmap, AList.insert_singleton_eq]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ Prod.map id AList.toFinmap (AList.extract a s₁) = Prod.map id AList.toFinmap (AList.extract a s₂)
[PROOFSTEP]
simp [perm_lookup p, toFinmap_eq, perm_erase p]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ extract a ⟦s⟧ = (lookup a ⟦s⟧, erase a ⟦s⟧)
[PROOFSTEP]
simp [extract]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₁ ∪ s₂⟧
[PROOFSTEP]
simp [(· ∪ ·), union]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α), a ∈ keys (⟦s₁⟧ ∪ ⟦s₂⟧) ↔ a ∈ keys ⟦s₁⟧ ∪ keys ⟦s₂⟧
[PROOFSTEP]
simp [keys]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
by_cases h' : a ∈ s₁
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
rw [lookup_union_left h']
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : ¬a ∈ s₂
h' : ¬a ∈ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁
[PROOFSTEP]
rw [lookup_union_right h', lookup_eq_none.mpr h, lookup_eq_none.mpr h']
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧
[PROOFSTEP]
simp [AList.insert_union]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ s₃✝ : Finmap β
s₁ s₂ s₃ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ ∪ ⟦s₃⟧ = ⟦s₁⟧ ∪ (⟦s₂⟧ ∪ ⟦s₃⟧)
[PROOFSTEP]
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ∅ ∪ ⟦s₁⟧ = ⟦s₁⟧
[PROOFSTEP]
rw [← empty_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
[PROOFSTEP]
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ∅ = ⟦s₁⟧
[PROOFSTEP]
rw [← empty_toFinmap]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧
[PROOFSTEP]
simp [-empty_toFinmap, AList.toFinmap_eq, union_toFinmap, AList.union_assoc]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
subst a
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ lookup x (erase x s ∪ singleton x b) = lookup x s
[PROOFSTEP]
rw [lookup_union_right not_mem_erase_self, lookup_singleton_eq, h]
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
have : x ∉ singleton a b := by rwa [mem_singleton]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ ¬x ∈ singleton a b
[PROOFSTEP]
rwa [mem_singleton]
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : ¬x ∈ singleton a b
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s
[PROOFSTEP]
rw [lookup_union_left_of_not_in this, lookup_erase_ne h']
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y : Finmap β
⊢ Decidable (Disjoint x y)
[PROOFSTEP]
dsimp only [Disjoint]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y : Finmap β
⊢ Decidable (∀ (x_1 : α), x_1 ∈ x → ¬x_1 ∈ y)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ Disjoint (x ∪ y) z ↔ Disjoint x z ∧ Disjoint y z
[PROOFSTEP]
simp [Disjoint, Finmap.mem_union, or_imp, forall_and]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ Disjoint x (y ∪ z) ↔ Disjoint x y ∧ Disjoint x z
[PROOFSTEP]
rw [Disjoint.symm_iff, disjoint_union_left, Disjoint.symm_iff _ x, Disjoint.symm_iff _ x]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ Disjoint ⟦s₁⟧ ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : Disjoint ⟦s₁⟧ ⟦s₂⟧
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧
[PROOFSTEP]
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ s₁ = s₂
[PROOFSTEP]
apply ext_lookup
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
⊢ ∀ (x : α), lookup x s₁ = lookup x s₂
[PROOFSTEP]
intro x
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
have : (s₁ ∪ s₃).lookup x = (s₂ ∪ s₃).lookup x := h'' ▸ rfl
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
by_cases hs₁ : x ∈ s₁
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
by_cases hs₂ : x ∈ s₂
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rwa [lookup_union_left_of_not_in (h' _ hs₂), lookup_union_left hs₂] at this
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : Disjoint s₁ s₃
h' : Disjoint s₂ s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : ¬x ∈ s₁
hs₂ : ¬x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
[PROOFSTEP]
rw [lookup_eq_none.mpr hs₁, lookup_eq_none.mpr hs₂]


[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x : α
⊢ List.indexOf x xs < List.length xs
[PROOFSTEP]
rw [List.indexOf_lt_length]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x : α
⊢ x ∈ xs
[PROOFSTEP]
apply h
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x : α
⊢ (fun x =>
        match x with
        | { val := i, isLt := h } => List.nthLe xs i h)
      ((fun x => { val := List.indexOf x xs, isLt := (_ : List.indexOf x xs < List.length xs) }) x) =
    x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h✝ : ∀ (x : α), x ∈ xs
h' : List.Nodup xs
x✝ : Fin (List.length xs)
i : ℕ
h : i < List.length xs
⊢ (fun x => { val := List.indexOf x xs, isLt := (_ : List.indexOf x xs < List.length xs) })
      ((fun x =>
          match x with
          | { val := i, isLt := h } => List.nthLe xs i h)
        { val := i, isLt := h }) =
    { val := i, isLt := h }
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
⊢ ∀ (x : α), x ∈ List.dedup xs
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ∃ a, ↑equiv.symm a = x
[PROOFSTEP]
exists equiv x
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x : α
⊢ ↑equiv.symm (↑equiv x) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (toList α)
[PROOFSTEP]
simp [toList]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑equiv.symm) (List.finRange (card α)))
[PROOFSTEP]
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.map (↑equiv.symm) (List.finRange (card α)))
[PROOFSTEP]
apply List.Nodup.map
[GOAL]
case hf
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ Injective ↑equiv.symm
[PROOFSTEP]
apply Equiv.injective
[GOAL]
case a
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ List.Nodup (List.finRange (card α))
[PROOFSTEP]
apply List.nodup_finRange
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
⊢ ∀ (x : α), x ∈ List.map f (toList β)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.8688
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ ∃ a, f a = x✝
[PROOFSTEP]
exact h _
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
⊢ ∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ x ∈ List.filterMap (partialInv f) (toList β)
[PROOFSTEP]
simp only [mem_toList, true_and_iff, List.mem_filterMap]
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ ∃ a, partialInv f a = some x
[PROOFSTEP]
use f x
[GOAL]
case h
α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.11794
β : Type ?u.11876
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
x : α
⊢ partialInv f (f x) = some x
[PROOFSTEP]
simp only [h, Function.partialInv_left]
[GOAL]
α : Type u
β : α → Type v
x : PUnit
⊢ x ∈ [PUnit.unit]
[PROOFSTEP]
cases x
[GOAL]
case unit
α : Type u
β : α → Type v
⊢ PUnit.unit ∈ [PUnit.unit]
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.13079
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u
β✝ : α → Type v
β : Type ?u.13079
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α ⊕ β
⊢ x ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
cases x
[GOAL]
case inl
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u
β✝ : α → Type v
β : Type ?u.16461
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
[PROOFSTEP]
induction' xs with xs_hd generalizing s
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s ∈ enum [] ↔ ∀ (x : α), x ∈ s → x ∈ []
[PROOFSTEP]
simp [*, Finset.enum]
[GOAL]
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ s ∈ enum (xs_hd :: tail✝) ↔ ∀ (x : α), x ∈ s → x ∈ xs_hd :: tail✝
[PROOFSTEP]
simp [*, Finset.enum]
[GOAL]
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), x ∈ s → False
[PROOFSTEP]
simp [Finset.eq_empty_iff_forall_not_mem]
[GOAL]
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
rintro ⟨a, h, h'⟩ x hx
[GOAL]
case cons.mp.intro.intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
h' : s = a ∨ s = {xs_hd} ∪ a
x : α
hx : x ∈ s
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
cases' h' with _ h' a b
[GOAL]
case cons.mp.intro.intro.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
right
[GOAL]
case cons.mp.intro.intro.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ tail✝
[PROOFSTEP]
apply h
[GOAL]
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ a
[PROOFSTEP]
subst a
[GOAL]
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
x : α
hx : x ∈ s
h : ∀ (x : α), x ∈ s → x ∈ tail✝
⊢ x ∈ s
[PROOFSTEP]
exact hx
[GOAL]
case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h' : s = {xs_hd} ∪ a
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
simp only [h', mem_union, mem_singleton] at hx ⊢
[GOAL]
case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd ∨ x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
cases' hx with hx hx'
[GOAL]
case cons.mp.intro.intro.inr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
exact Or.inl hx
[GOAL]
case cons.mp.intro.intro.inr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx' : x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
[PROOFSTEP]
exact Or.inr (h _ hx')
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
[PROOFSTEP]
intro h
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
[PROOFSTEP]
exists s \ ({ xs_hd } : Finset α)
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s \ {xs_hd} → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
simp only [and_imp, mem_sdiff, mem_singleton]
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
simp only [or_iff_not_imp_left] at h
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
[PROOFSTEP]
exists h
[GOAL]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
by_cases h : xs_hd ∈ s
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
have : { xs_hd } ⊆ s
[GOAL]
case this
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ {xs_hd} ⊆ s
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
[GOAL]
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset, eq_self_iff_true]
[GOAL]
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
[PROOFSTEP]
left
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd}
[PROOFSTEP]
symm
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s \ {xs_hd} = s
[PROOFSTEP]
simp only [sdiff_eq_self]
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s ∩ {xs_hd} ⊆ ∅
[PROOFSTEP]
intro a
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s ∩ {xs_hd} → a ∈ ∅
[PROOFSTEP]
simp only [and_imp, mem_inter, mem_singleton]
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s → a = xs_hd → a ∈ ∅
[PROOFSTEP]
rintro h₀ rfl
[GOAL]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
a : α
h₀ : a ∈ s
h✝ : ∀ (x : α), x ∈ s → ¬x = a → x ∈ tail✝
h : ¬a ∈ s
⊢ a ∈ ∅
[PROOFSTEP]
exact (h h₀).elim
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : Finset α
⊢ x✝ ∈ enum (toList α)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : { x // p x }),
    x ∈ List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)
[PROOFSTEP]
rintro ⟨x, h⟩
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ { val := x, property := h } ∈
    List.filterMap (fun x => if h : p x then some { val := x, property := h } else none) (toList α)
[PROOFSTEP]
simp
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ ∃ a, (if h : p a then some { val := a, property := h } else none) = some { val := x, property := h }
[PROOFSTEP]
exists x
[GOAL]
case mk
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ (if h : p x then some { val := x, property := h } else none) = some { val := x, property := h }
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
⊢ ∀ (x : Sigma β), x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))
[PROOFSTEP]
intro x
[GOAL]
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
x : Sigma β
⊢ x ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } ∈ List.bind (toList α) fun a => List.map (Sigma.mk a) (toList (β a))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Type v
inst✝¹ : (a : α) → FinEnum (β a)
inst✝ : Decidable α
h : α
x✝ : (a : α) ×' β a
a : α
Ba : β a
⊢ { fst := a, snd := Ba } ∈ List.map (PSigma.mk h) (toList (β h))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ a, β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ a, β a
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } ∈ [{ fst := (_ : α), snd := (_ : β (_ : α)) }]
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : α), x ∈ map (Equiv.toEmbedding equiv.symm) univ
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map (Equiv.toEmbedding equiv.symm) univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : α → Type v
inst✝ : DecidableEq α
x : α
xs : List α
y : β x
f : (a : α) → a ∈ xs → β a
b : α
h : b ∈ x :: xs
h' : b = x
⊢ β x = β b
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f : (a : α) → a ∈ xs → β a
⊢ f ∈ pi xs fun x => toList (β x)
[PROOFSTEP]
induction' xs with xs_hd xs_tl xs_ih
[GOAL]
case nil
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
f : (a : α) → a ∈ [] → β a
⊢ f ∈ pi [] fun x => toList (β x)
[PROOFSTEP]
simp [pi, -List.map_eq_map, monad_norm, functor_norm]
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ f ∈ pi (xs_hd :: xs_tl) fun x => toList (β x)
[PROOFSTEP]
simp [pi, -List.map_eq_map, monad_norm, functor_norm]
[GOAL]
case nil
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
f : (a : α) → a ∈ [] → β a
⊢ f = fun x h => False.elim (_ : False)
[PROOFSTEP]
ext a ⟨⟩
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (∃ a_1, a = Pi.cons xs_hd xs_tl a_1) ∧ ∃ a_1, (a_1 ∈ pi xs_tl fun x => toList (β x)) ∧ f = a a_1
[PROOFSTEP]
exists Pi.cons xs_hd xs_tl (f _ (List.mem_cons_self _ _))
[GOAL]
case cons
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ (∃ a, Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) = Pi.cons xs_hd xs_tl a) ∧
    ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
constructor
[GOAL]
case cons.left
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) = Pi.cons xs_hd xs_tl a
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ ∃ a, (a ∈ pi xs_tl fun x => toList (β x)) ∧ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) a
[PROOFSTEP]
exists Pi.tail f
[GOAL]
case cons.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ (Pi.tail f ∈ pi xs_tl fun x => toList (β x)) ∧
    f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f)
[PROOFSTEP]
constructor
[GOAL]
case cons.right.left
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ Pi.tail f ∈ pi xs_tl fun x => toList (β x)
[PROOFSTEP]
apply xs_ih
[GOAL]
case cons.right.right
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
⊢ f = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f)
[PROOFSTEP]
ext x h
[GOAL]
case cons.right.right.h.h
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
⊢ f x h = Pi.cons xs_hd xs_tl (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl)) (Pi.tail f) x h
[PROOFSTEP]
simp [Pi.cons]
[GOAL]
case cons.right.right.h.h
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
⊢ f x h =
    if h' : x = xs_hd then cast (_ : β xs_hd = β x) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
    else Pi.tail f x (_ : x ∈ xs_tl)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
h✝ : x = xs_hd
⊢ f x h = cast (_ : β xs_hd = β x) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
h : xs_hd ∈ xs_hd :: xs_tl
⊢ f xs_hd h = cast (_ : β xs_hd = β xs_hd) (f xs_hd (_ : xs_hd ∈ xs_hd :: xs_tl))
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β✝ : α → Type v
β : α → Type (max u u_1)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
xs : List α
f✝ : (a : α) → a ∈ xs → β a
xs_hd : α
xs_tl : List α
xs_ih : ∀ (f : (a : α) → a ∈ xs_tl → β a), f ∈ pi xs_tl fun x => toList (β x)
f : (a : α) → a ∈ xs_hd :: xs_tl → β a
x : α
h : x ∈ xs_hd :: xs_tl
h✝ : ¬x = xs_hd
⊢ f x h = Pi.tail f x (_ : x ∈ xs_tl)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u v)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β
[PROOFSTEP]
simp [pi.enum]
[GOAL]
α : Type u
β✝ : α → Type v
β : α → Type (max u v)
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ ∃ a, (a ∈ pi (toList α) fun x => toList (β x)) ∧ (fun x => a x (_ : x ∈ toList α)) = f
[PROOFSTEP]
refine' ⟨fun a _ => f a, mem_pi _ _, rfl⟩
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
⊢ ∀ (x : (hp : p) → α hp), x ∈ List.map (fun x x_1 => x) (toList (α hp))
[PROOFSTEP]
intro x
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ List.map (fun x x_1 => x) (toList (α hp))
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ ∃ a, (fun x => a) = x
[PROOFSTEP]
exact ⟨x hp, rfl⟩
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
⊢ ∀ (x : (hp : p) → α hp), x ∈ [fun hp' => False.elim (_ : False)]
[PROOFSTEP]
intro
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
⊢ x✝ ∈ [fun hp' => False.elim (_ : False)]
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
⊢ x✝ = fun hp' => False.elim (_ : False)
[PROOFSTEP]
ext hp'
[GOAL]
case h
α✝ : Type u
β : α✝ → Type v
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
x✝ : (hp : p) → α hp
hp' : p
⊢ x✝ hp' = False.elim (_ : False)
[PROOFSTEP]
cases hp hp'