[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range n = []
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, List.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ insert a s = a ::ₘ s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
⊢ Multiset.count a✝ (insert a s) = Multiset.count a✝ (a ::ₘ s)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, Multiset.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ Multiset.range n = n' ::ₘ Multiset.range n'
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ insert a s = Finset.cons a s h
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
a✝ : α
⊢ a✝ ∈ insert a s ↔ a✝ ∈ Finset.cons a s h
[PROOFSTEP]
simp
[GOAL]
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅
[PROOFSTEP]
rw [pn.out, Nat.cast_zero, Finset.range_zero]
[GOAL]
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = Nat.succ n'
⊢ Finset.range n = Finset.cons n' (Finset.range n') (_ : ¬n' ∈ Finset.range n')
[PROOFSTEP]
rw [pn.out, Nat.cast_id, pn', Finset.range_succ, Finset.insert_eq_cons]
[GOAL]
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
⊢ Finset.univ = elems
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems
[PROOFSTEP]
simpa using complete x
[GOAL]
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ Finset.sum ∅ f = ↑0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ Finset.prod ∅ f = ↑1
[PROOFSTEP]
simp
